Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.dLpNorm_prod_le

APAP.Prereqs.Inner.Hoelder.Discrete · APAP/Prereqs/Inner/Hoelder/Discrete.lean:112 to 131

Source documentation

Hölder's inequality, finitary case.

Exact Lean statement

lemma dLpNorm_prod_le {ι : 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 dLpNorm_prod_le {ι : 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 s using Finset.cons_induction generalizing q with  | empty => cases not_nonempty_empty hs  | cons i s hi ih =>    obtain rfl | hs := s.eq_empty_or_nonempty    · simp only [sum_cons, sum_empty, add_zero, inv_inj] at hpq      simp [← hpq]    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 [dLpNorm_mul_le (p i) ↑(∑ i ∈ s, (p i)⁻¹)⁻¹, ih hs]    rw [← ENNReal.coe_inv, inv_inv]    · push_cast      congr! with i      exact (ENNReal.coe_inv <| hp _).symm    · simpa [hp]