MeasureTheory.wInner_one_le_dLpNorm_mul_dLpNorm

lemma wInner_one_le_dLpNorm_mul_dLpNorm (p q : ℝ≥0∞) [p.HolderConjugate q] :    ⟪f, g⟫_[ℝ] ≤ ‖f‖_[p] * ‖g‖_[q] := by  have hp0 : p ≠ 0 := ENNReal.HolderConjugate.ne_zero p q  have hq0 : q ≠ 0 := ENNReal.HolderConjugate.ne_zero q p  have hwInner : ⟪f, g⟫_[ℝ] = ∑ i, f i * g i := by simp [wInner_one_eq_sum, mul_comm]  have hfg i : f i * g i ≤ ‖f i‖ * ‖g i‖ :=    (le_abs_self _).trans_eq (by rw [abs_mul]; simp [Real.norm_eq_abs])  obtain rfl | hpi := eq_or_ne p ∞  · obtain rfl : q = 1 := (ENNReal.HolderConjugate.eq_top_iff_eq_one ∞ q).mp rfl    simp only [hwInner, dL1Norm_eq_sum_norm, norm_eq_abs, dLinftyNorm_eq_iSup_norm, mul_sum]    gcongr ∑ _, ?_ with i    grw [le_abs_self (_ * _), abs_mul, ← le_ciSup (Finite.bddAbove_range _)]  obtain rfl | hqi := eq_or_ne q ∞  · obtain rfl : p = 1 := (ENNReal.HolderConjugate.eq_top_iff_eq_one ∞ p).mp rfl    simp only [hwInner, dL1Norm_eq_sum_norm, norm_eq_abs, dLinftyNorm_eq_iSup_norm, sum_mul]    gcongr ∑ _, ?_ with i    grw [le_abs_self (_ * _), abs_mul, ← le_ciSup (Finite.bddAbove_range _)]  have hpr : 0 < p.toReal := ENNReal.toReal_pos hp0 hpi  have hqr : 0 < q.toReal := ENNReal.toReal_pos hq0 hqi  have hreal : Real.HolderConjugate p.toReal q.toReal := by    simpa using ENNReal.HolderTriple.toReal (p := p) (q := q) (r := 1) hpr hqr  rw [hwInner, dLpNorm_eq_sum_norm' hp0 hpi, dLpNorm_eq_sum_norm' hq0 hqi]  simpa using Real.inner_le_Lp_mul_Lq Finset.univ f g hreal