Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.AESublinearOn.toReal

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:339 to 350

Mathematical statement

Exact Lean statement

lemma toReal {T : (α → ε₁) → α' → ℝ≥0∞}
    {P : (α → ε₁) → Prop}
    {A : ℝ≥0∞} (h : AESublinearOn T P A ν)
    (hP : ∀ (u : α → ε₁), P u → ∀ᵐ x ∂ν, T u x ≠ ∞) :
    AESublinearOn (T · · |>.toReal) P A ν

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma toReal {T : (α → ε₁) → α' → ℝ≥0∞}    {P : (α → ε₁) → Prop}    {A : ℝ≥0∞} (h : AESublinearOn T P A ν)    (hP : ∀ (u : α → ε₁), P u → ∀ᵐ x ∂ν, T u x ≠ ∞) :    AESublinearOn (T · · |>.toReal) P A ν := by  refine ⟨fun f g hf hg ↦ ?_, fun f c hf ↦ ?_⟩  · filter_upwards [h.1 f g hf hg, hP f hf, hP g hg] with x hx hfx hgx    simp only [ne_eq, hfx, not_false_eq_true, Real.enorm_toReal, hgx] at hx ⊢    exact enorm_toReal_le.trans hx  · filter_upwards [h.2 f c hf, hP f hf] with x hx hfx    rw [hx, Pi.smul_apply, toReal_smul]    rfl