Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.hasStrongType_iSup_of_monotone

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:565 to 579

Mathematical statement

Exact Lean statement

lemma hasStrongType_iSup_of_monotone {f : ℕ → (α → ε₁) → (α' → ℝ≥0∞)} (hf : Monotone f)
    (hstf : ∀ n, HasStrongType (f n) p p' μ ν c) :
    HasStrongType (fun u x => ⨆ n, f n u x) p p' μ ν c

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasStrongType_iSup_of_monotone {f : ℕ → (α → ε₁) → (α' → ℝ≥0∞)} (hf : Monotone f)    (hstf : ∀ n, HasStrongType (f n) p p' μ ν c) :    HasStrongType (fun u x => ⨆ n, f n u x) p p' μ ν c := by  intro v mlpv  constructor  · apply AEMeasurable.aestronglyMeasurable    -- should StronglyMeasurable.iSup exist?    apply AEMeasurable.iSup    exact (hstf · v mlpv |>.left.aemeasurable)  · rw [eLpNorm_iSup']    · exact iSup_le fun n => hstf n v mlpv |>.right    · exact fun n => hstf n v mlpv |>.left.aemeasurable    · apply ae_of_all      intro a      exact (hf.apply₂ _).apply₂ _