Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm

Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.CompareExp · Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean:97 to 122

Source documentation

Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x).

Exact Lean statement

theorem eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm {p q r : ℝ≥0∞}
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0)
    (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ) [hpqr : HolderTriple p q r] :
    eLpNorm (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm f p μ * eLpNorm g q μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm {p q r : ℝ≥0∞}    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0)    (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ) [hpqr : HolderTriple p q r] :    eLpNorm (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm f p μ * eLpNorm g q μ := by  have hpqr := hpqr.one_div_eq  obtain (rfl | rfl | hp) := ENNReal.trichotomy p  · simp_all  · have : r = q := by simpa using hpqr    exact this ▸ eLpNorm_le_eLpNorm_top_mul_eLpNorm' r f hg b c h  obtain (rfl | rfl | hq) := ENNReal.trichotomy q  · simp_all  · have : r = p := by simpa using hpqr    exact this ▸ eLpNorm_le_eLpNorm_mul_eLpNorm_top'' p hf g b c h  obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp  obtain ⟨hq₁, hq₂⟩ := ENNReal.toReal_pos_iff.mp hq  have hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal := by    have := congr(ENNReal.toReal $(hpqr))    rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this    simpa  have hr : 0 < r.toReal := one_div_pos.mp <| by rw [hpqr']; positivity  obtain ⟨hr₁, hr₂⟩ := ENNReal.toReal_pos_iff.mp hr  have hrp : r.toReal < p.toReal := lt_of_one_div_lt_one_div hp <|    hpqr' ▸ lt_add_of_pos_right _ (by positivity)  rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']  · exact eLpNorm'_le_eLpNorm'_mul_eLpNorm'' hf hg b c h hr hrp hpqr'  all_goals first | positivity | finiteness