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

MeasureTheory.AESubadditiveOn.biSup

Carleson.ToMathlib.RealInterpolation.Main Β· Carleson/ToMathlib/RealInterpolation/Main.lean:141 to 173

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 β‰  ∞)
    (hP : βˆ€ {f g : Ξ± β†’ Ρ₁}, P f β†’ P g β†’ P (f + g))
    {A : ℝβ‰₯0∞} (h : βˆ€ i ∈ 𝓑, AESubadditiveOn (T i) P A Ξ½) :
    AESubadditiveOn (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 β‰  ∞)    (hP : βˆ€ {f g : Ξ± β†’ Ρ₁}, P f β†’ P g β†’ P (f + g))    {A : ℝβ‰₯0∞} (h : βˆ€ i ∈ 𝓑, AESubadditiveOn (T i) P A Ξ½) :    AESubadditiveOn (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)  -- rcases lt_or_le A 0 with A0 | A0  -- Β· refine AESubadditiveOn.zero hP A (fun f hf ↦ ?_)  --   have h (i : ΞΉ) (hi : i ∈ 𝓑) := (h i hi).neg _ A0  --   simp_rw [Set.forall_in_swap, imp.swap, ← imp_forall_iff] at h hT'  --   filter_upwards [(ae_ball_iff h𝓑).mpr (h f hf), (ae_ball_iff h𝓑).mpr (hT' f hf)] with x hx hx'  --   simp only [Pi.zero_apply, toReal_eq_zero_iff, ENNReal.iSup_eq_zero]  --   refine Or.inl fun i hi ↦ ?_  --   have := (ENNReal.toReal_eq_zero_iff _).mp (hx i hi)  --   tauto  intro f g hf hg  simp_rw [AESubadditiveOn] at h  conv at hT' => enter [i]; rw [forall_comm]  rw [forall_comm] at hT'; rw [forallβ‚‚_comm] at h  simp_rw [imp.swap, ← imp_forall_iff] at h hT'  specialize h f hf g hg  simp_rw [enorm_eq_self] at h ⊒  filter_upwards [hT f hf, hT g hg, (ae_ball_iff h𝓑).mpr h, (ae_ball_iff h𝓑).mpr (hT' f hf),    (ae_ball_iff h𝓑).mpr (hT' g hg), (ae_ball_iff h𝓑).mpr (hT' (f + g) (hP hf hg))] with x hTfx hTgx hx hT'fx hT'gx hT'fgx  simp_rw [iSup_le_iff]  intro i hi  specialize hx i hi  apply hx.trans  gcongr <;> apply le_biSup _ hi