Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.wnorm_iSup_of_monotone

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:267 to 281

Mathematical statement

Exact Lean statement

lemma wnorm_iSup_of_monotone {α : Type*} [MeasurableSpace α] {p : ℝ≥0∞} (hp : p ≠ 0) (f : ℕ → α → ℝ≥0∞)
    (hf : Monotone f) (μ : Measure α) : wnorm (fun x => ⨆ n, f n x) p μ = ⨆ n, wnorm (f n) p μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma wnorm_iSup_of_monotone {α : Type*} [MeasurableSpace α] {p : ℝ≥0∞} (hp : p ≠ 0) (f : ℕ → α → ℝ≥0∞)    (hf : Monotone f) (μ : Measure α) : wnorm (fun x => ⨆ n, f n x) p μ = ⨆ n, wnorm (f n) p μ := by  unfold wnorm wnorm' distribution  split_ifs with hp'  · apply eLpNormEssSup_iSup  · rw [iSup_comm]; congr with t    rw [←ENNReal.mul_iSup]; congr    rw [←(iSup_rpow (toReal_pos hp hp' |> inv_pos_of_pos))]; congr    simp only [enorm_eq_self]    rw [←Monotone.measure_iUnion, iUnion_setOf]    · congr with x      exact lt_iSup_iff    · apply monotone_setOf      intro x      exact monotone_lt.comp (hf.apply₂ x)