MeasureTheory.cLpNorm_mul_le

lemma cLpNorm_mul_le (p q : ℝ≥0∞) (_hr₀ : r ≠ 0) [hpqr : ENNReal.HolderTriple p q r] :    ‖f * g‖ₙ_[r] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := by  cases nonempty_fintype α  set μ := ProbabilityTheory.uniformOn (Set.univ : Set α) with hμ_def  have hμfin : IsFiniteMeasure μ := by rw [hμ_def]; infer_instance  have hm_r : MemLp (f * g) r μ := MemLp.of_discrete  have hm_p : MemLp f p μ := MemLp.of_discrete  have hm_q : MemLp g q μ := MemLp.of_discrete  have hbd : ∀ᵐ x ∂μ, ‖f x * g x‖₊ ≤ (1 : NNReal) * ‖f x‖₊ * ‖g x‖₊ :=    .of_forall fun x ↦ by rw [one_mul]; exact nnnorm_mul_le _ _  have key : eLpNorm (fun x ↦ f x * g x) r μ      ≤ ((1 : NNReal) : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ :=    eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm (p := p) (q := q) (r := r)      hm_p.aestronglyMeasurable hm_q.aestronglyMeasurable (· * ·) 1 hbd  change lpNorm _ _ μ ≤ lpNorm _ _ μ * lpNorm _ _ μ  rw [← toReal_eLpNorm hm_r.aestronglyMeasurable,      ← toReal_eLpNorm hm_p.aestronglyMeasurable,      ← toReal_eLpNorm hm_q.aestronglyMeasurable,      ← ENNReal.toReal_mul]  apply ENNReal.toReal_mono  · exact ENNReal.mul_ne_top hm_p.eLpNorm_ne_top hm_q.eLpNorm_ne_top  · simpa [Pi.mul_def] using key