Skip to main content
therefore
Sign inSign up
Open navigation
fpvandoorn/carleson
Source indexedlemma Β· leanprover/lean4:v4.32.0

MeasureTheory.AESublinearOn.biSup

Carleson.ToMathlib.RealInterpolation.Main Β· Carleson/ToMathlib/RealInterpolation/Main.lean:263 to 282

Mathematical statement

Exact Lean statement

lemma biSup {ΞΉ : Type*} {𝓑 : Set ΞΉ} (h𝓑 : 𝓑.Countable) {T : ΞΉ β†’ (Ξ± β†’ Ρ₁) β†’ Ξ±' β†’ ℝβ‰₯0∞}
    {P : (Ξ± β†’ Ρ₁) β†’ Prop} (hT : βˆ€ (u : Ξ± β†’ Ρ₁), P u β†’ βˆ€α΅ x βˆ‚Ξ½, ⨆ i ∈ 𝓑, T i u x β‰  ∞)
    (h_add : βˆ€ {f g : Ξ± β†’ Ρ₁}, P f β†’ P g β†’ P (f + g))
    (h_smul : βˆ€ {f : Ξ± β†’ Ρ₁} {c : ℝβ‰₯0}, P f β†’ P (c β€’ f))
    {A : ℝβ‰₯0∞} (h : βˆ€ i ∈ 𝓑, AESublinearOn (T i) P A Ξ½) :
    AESublinearOn (fun u x ↦ ⨆ i ∈ 𝓑, T i u x) P A Ξ½

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma biSup {ΞΉ : Type*} {𝓑 : Set ΞΉ} (h𝓑 : 𝓑.Countable) {T : ΞΉ β†’ (Ξ± β†’ Ρ₁) β†’ Ξ±' β†’ ℝβ‰₯0∞}    {P : (Ξ± β†’ Ρ₁) β†’ Prop} (hT : βˆ€ (u : Ξ± β†’ Ρ₁), P u β†’ βˆ€α΅ x βˆ‚Ξ½, ⨆ i ∈ 𝓑, T i u x β‰  ∞)    (h_add : βˆ€ {f g : Ξ± β†’ Ρ₁}, P f β†’ P g β†’ P (f + g))    (h_smul : βˆ€ {f : Ξ± β†’ Ρ₁} {c : ℝβ‰₯0}, P f β†’ P (c β€’ f))    {A : ℝβ‰₯0∞} (h : βˆ€ i ∈ 𝓑, AESublinearOn (T i) P A Ξ½) :    AESublinearOn (fun u x ↦ ⨆ i ∈ 𝓑, T i u x) P A Ξ½ := by  have hT' : βˆ€ i ∈ 𝓑, βˆ€ (u : Ξ± β†’ Ρ₁), P u β†’ βˆ€α΅ x βˆ‚Ξ½, T i u x β‰  ∞ := by    intro i hi f hf    filter_upwards [hT f hf] with x hx    rw [ne_eq, eq_top_iff] at hx ⊒    exact fun h ↦ hx <| h.trans (le_biSup (fun i ↦ T i f x) hi)  refine ⟨AESubadditiveOn.biSup h𝓑 hT h_add (fun i hi ↦ (h i hi).1), fun f c hf ↦ ?_⟩  conv at hT' => enter [i]; rw [forall_comm]  rw [forall_comm] at hT'; simp_rw [imp.swap, ← imp_forall_iff] at hT'  filter_upwards [(ae_ball_iff h𝓑).mpr (fun i hi ↦ (h i hi).2 f c hf),    (ae_ball_iff h𝓑).mpr (hT' f hf), (ae_ball_iff h𝓑).mpr (hT' (c β€’ f) (h_smul hf))] with x hx hT'fx hT'cfx  simp_rw [Pi.smul_apply, ENNReal.smul_iSup]  refine biSup_congr (fun i hi ↦ ?_)  specialize hx i hi  simpa only [Pi.smul_apply, smul_eq_mul] using hx