MeasureTheory.wInner_cWeight_le_cLpNorm_mul_cLpNorm

lemma wInner_cWeight_le_cLpNorm_mul_cLpNorm (p q : ℝ≥0∞) [p.HolderConjugate q] :    ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := by  -- Step 1: `⟪f, g⟫ₙ_[ℝ] ≤ ⟪|f|, |g|⟫ₙ_[ℝ]` (dominate by absolute value)  have h_abs : ⟪f, g⟫ₙ_[ℝ] ≤ ⟪fun i ↦ |f i|, fun i ↦ |g i|⟫ₙ_[ℝ] := by    simp_rw [wInner_cWeight_eq_expect]    refine expect_le_expect fun i _ ↦ ?_    exact (le_abs_self _).trans (abs_mul _ _).le  refine h_abs.trans ?_  -- Step 2: Now both arguments are nonneg; the target becomes the Hölder inequality  -- `⟪|f|, |g|⟫ₙ_[ℝ] ≤ ‖|f|‖ₙ_[p] * ‖|g|‖ₙ_[q]` which we rewrite back to f, g using  -- `cLpNorm_abs` / `cLpNorm_fun_abs`.  have hfabs : ‖fun i ↦ |f i|‖ₙ_[p] = ‖f‖ₙ_[p] := by    simpa using cLpNorm_fun_abs (f := f) (p := p) .of_discrete  have hgabs : ‖fun i ↦ |g i|‖ₙ_[q] = ‖g‖ₙ_[q] := by    simpa using cLpNorm_fun_abs (f := g) (p := q) .of_discrete  rw [← hfabs, ← hgabs]  rw [show ⟪fun i ↦ |f i|, fun i ↦ |g i|⟫ₙ_[ℝ]        = ‖(fun i ↦ |f i|) * (fun i ↦ |g i|)‖ₙ_[1] from        (cL1Norm_mul_of_nonneg (f := fun i ↦ |f i|) (g := fun i ↦ |g i|)          (fun i ↦ abs_nonneg _) (fun i ↦ abs_nonneg _)).symm]  exact cLpNorm_mul_le p q one_ne_zero