Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.hasWeakType_iSup_of_monotone

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:496 to 507

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasWeakType_iSup_of_monotone {f : ℕ → (α → ε₁) → (α' → ℝ≥0∞)} (hf : Monotone f)    (hp' : p' ≠ 0) (hwtf : ∀ n, HasWeakType (f n) p p' μ ν c) :    HasWeakType (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 (hwtf · v mlpv |>.left.aemeasurable)  · rw [wnorm_iSup_of_monotone hp']    · exact iSup_le fun n => hwtf n v mlpv |>.right    · exact hf.apply₂ v