Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.truncCompl_Lp_Lq_lower

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:872 to 886

Source documentation

If f is in Lp, the complement of the truncation is in Lq for q ≤ p.

Exact Lean statement

lemma truncCompl_Lp_Lq_lower
    (hp : p ≠ ⊤) (hpq : q ∈ Ioc 0 p) (ht : 0 < t) (hf : MemLp f p μ) :
    MemLp (trnc ⊥ f t) q μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma truncCompl_Lp_Lq_lower    (hp : p ≠ ⊤) (hpq : q ∈ Ioc 0 p) (ht : 0 < t) (hf : MemLp f p μ) :    MemLp (trnc ⊥ f t) q μ := by  have q_ne_top : q ≠ ∞ := ne_top_of_le_ne_top hp hpq.2  by_cases ht' : t = ∞  · simp [trnc, ht']  refine ⟨aestronglyMeasurable_trnc hf.1, ?_⟩  have : 0 < q.toReal := toReal_pos hpq.left.ne' q_ne_top  refine (rpow_lt_top_iff_of_pos this).mp ?_  refine lt_of_le_of_lt (estimate_eLpNorm_truncCompl hp hpq hf.1 ht) ?_  apply mul_lt_top  · push Not at ht'    finiteness  refine (rpow_lt_top_iff_of_pos ?_).mpr hf.2  exact toReal_pos (hpq.1.trans_le hpq.2).ne' hp