Source indexedlemma · leanprover/lean4:v4.32.0

wLpNorm_mono_right

APAP.Prereqs.LpNorm.Weighted · APAP/Prereqs/LpNorm/Weighted.lean:110 to 123

Source documentation

Monotonicity of weighted L^p norms in the exponent, for probability weights.

Exact Lean statement

@[gcongr]
lemma wLpNorm_mono_right
    (hw : ∑ i, (w i : ℝ≥0∞) = 1) (hpq : p ≤ q) (f : α → E) :
    ‖f‖_[p, w] ≤ ‖f‖_[q, w]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[gcongr]lemma wLpNorm_mono_right    (hw : ∑ i, (w i : ℝ≥0∞) = 1) (hpq : p ≤ q) (f : α → E) :    ‖f‖_[p, w] ≤ ‖f‖_[q, w] := by  have : IsProbabilityMeasure (Measure.sum fun i ↦ (w i : ℝ≥0) • Measure.dirac (i : α)) := by    rw [isProbabilityMeasure_iff, Measure.sum_apply _ MeasurableSet.univ]    simp [hw, ← Measure.coe_nnreal_smul]  rw [wLpNorm, wLpNorm,      ← toReal_eLpNorm (μ := Measure.sum fun i ↦ (w i : ℝ≥0) • Measure.dirac i)        (MemLp.of_discrete (p := p)).aestronglyMeasurable,      ← toReal_eLpNorm (μ := Measure.sum fun i ↦ (w i : ℝ≥0) • Measure.dirac i)        (MemLp.of_discrete (p := q)).aestronglyMeasurable]  exact ENNReal.toReal_mono (MemLp.of_discrete (p := q)).eLpNorm_ne_top    (eLpNorm_le_eLpNorm_of_exponent_le hpq (MemLp.of_discrete (p := p)).aestronglyMeasurable)