Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_iSup'

Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean:101 to 114

Source documentation

Monotone convergence applied to eLpNorms. AEMeasurable variant. Possibly imperfect hypotheses, particularly on p. Note that for p = ∞ the stronger statement in eLpNormEssSup_iSup holds.

Exact Lean statement

theorem eLpNorm_iSup' {α : Type*} [MeasurableSpace α] {μ : Measure α} {p : ℝ≥0∞}
    {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ) (h_mono : ∀ᵐ x ∂μ, Monotone fun n => f n x) :
    eLpNorm (fun x => ⨆ n, f n x) p μ = ⨆ n, eLpNorm (f n) p μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eLpNorm_iSup' {α : Type*} [MeasurableSpace α] {μ : Measure α} {p : ℝ≥0∞}    {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ) (h_mono : ∀ᵐ x ∂μ, Monotone fun n => f n x) :    eLpNorm (fun x => ⨆ n, f n x) p μ = ⨆ n, eLpNorm (f n) p μ := by  unfold eLpNorm  split_ifs with hp hp'  · simp  · apply eLpNormEssSup_iSup  · unfold eLpNorm'    have := ENNReal.toReal_pos hp hp'    rw [← iSup_rpow (by positivity), ← lintegral_iSup']    · congr 2 with a; rw [← iSup_rpow (by positivity)]; simp    · fun_prop    · filter_upwards [h_mono] with a ha m n hmn      beta_reduce; gcongr; simp only [enorm_eq_self]; apply ha hmn