Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.cLpNorm_prod_le

APAP.Prereqs.Inner.Hoelder.Compact · APAP/Prereqs/Inner/Hoelder/Compact.lean:148 to 168

Source documentation

Hölder's inequality, finitary case.

Exact Lean statement

lemma cLpNorm_prod_le [Finite α] {ι : Type*} {s : Finset ι} (hs : s.Nonempty)
    {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0)
    (q : ℝ≥0) (hpq : ∑ i ∈ s, ((p i)⁻¹ : ℝ≥0∞) = (q : ℝ≥0∞)⁻¹) (f : ι → α → 𝕜) :
    ‖∏ i ∈ s, f i‖ₙ_[q] ≤ ∏ i ∈ s, ‖f i‖ₙ_[p i]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cLpNorm_prod_le [Finite α] {ι : Type*} {s : Finset ι} (hs : s.Nonempty)    {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0)    (q : ℝ≥0) (hpq : ∑ i ∈ s, ((p i)⁻¹ : ℝ≥0∞) = (q : ℝ≥0∞)⁻¹) (f : ι → α → 𝕜) :    ‖∏ i ∈ s, f i‖ₙ_[q] ≤ ∏ i ∈ s, ‖f i‖ₙ_[p i] := by  induction hs using Finset.Nonempty.cons_induction generalizing q with  | singleton => simp_all  | cons i s hi hs ih =>  simp_rw [prod_cons]  rw [sum_cons, ← inv_inv (∑ _ ∈ _, _)] at hpq  have : ENNReal.HolderTriple (p i) ↑(∑ i ∈ s, (p i)⁻¹)⁻¹ q := ⟨by    simpa [ENNReal.coe_inv (by simpa [hp] :      (∑ j ∈ s, (p j)⁻¹ : ℝ≥0) ≠ 0), ENNReal.coe_inv, hp] using hpq⟩  grw [cLpNorm_mul_le (p i) ↑(∑ i ∈ s, (p i)⁻¹)⁻¹ , ih]  · rw [← ENNReal.coe_inv, inv_inv]    · push_cast      congr! with i      exact (ENNReal.coe_inv <| hp _).symm    · simpa [hp]  · norm_cast    rintro rfl    simp [hp] at hpq