Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.dLpNorm_mul_le

APAP.Prereqs.Inner.Hoelder.Discrete · APAP/Prereqs/Inner/Hoelder/Discrete.lean:103 to 109

Source documentation

Hölder's inequality, binary case.

Exact Lean statement

lemma dLpNorm_mul_le (p q : ℝ≥0∞) [p.HolderTriple q r] : ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dLpNorm_mul_le (p q : ℝ≥0∞) [p.HolderTriple q r] : ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q] := by  cases nonempty_fintype α  change lpNorm (f * g) r .count ≤ lpNorm f p .count * lpNorm g q .count  have hfg : AEStronglyMeasurable (f * g) .count := .of_discrete  grw [← toReal_eLpNorm .of_discrete, ← toReal_eLpNorm .of_discrete, ← toReal_eLpNorm .of_discrete,    ← ENNReal.toReal_mul, ← eLpNorm_mul_le_mul_eLpNorm (r := r) .of_discrete .of_discrete]  exact (ENNReal.mul_lt_top eLpNorm_lt_top_of_finite eLpNorm_lt_top_of_finite).ne