Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.combine_estimates₁

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:857 to 897

Mathematical statement

Exact Lean statement

lemma combine_estimates₁ {A : ℝ≥0} (hA : 0 < A)
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    [TopologicalSpace E₂] [ContinuousENorm E₂]
    {spf : ScaledPowerFunction}
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1)
    (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁)
    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
    (hf : MemLp f p μ) (hT : SubadditiveTrunc T A f ν)
    (h₁T : HasWeakType T p₁ q₁ μ ν C₁)
    (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
    (h₂T : PreservesAEStrongMeasurability T p (ν := ν) (μ := μ))
    (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤)
    (hspf : spf = spf_ch (toReal_mem_Ioo ht) hq₀q₁ hp₀.1 (lt_of_lt_of_le hp₀.1 hp₀.2) hp₁.1
        (lt_of_lt_of_le hp₁.1 hp₁.2) hp₀p₁.ne hC₀ hC₁ hF) :
    eLpNorm (T f) q ν ≤
    ENNReal.ofReal (2 * A) * q ^ q⁻¹.toReal *
    (((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ +
    (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹)) ^ q⁻¹.toReal *
    C₀ ^ (1 - t).toReal * C₁ ^ t.toReal * eLpNorm f p μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma combine_estimates₁ {A : ℝ≥0} (hA : 0 < A)    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    [TopologicalSpace E₂] [ContinuousENorm E₂]    {spf : ScaledPowerFunction}    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1)    (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)    (hf : MemLp f p μ) (hT : SubadditiveTrunc T A f ν)    (h₁T : HasWeakType T p₁ q₁ μ ν C₁)    (h₀T : HasWeakType T p₀ q₀ μ ν C₀)    (h₂T : PreservesAEStrongMeasurability T p (ν := ν) (μ := μ))    (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤)    (hspf : spf = spf_ch (toReal_mem_Ioo ht) hq₀q₁ hp₀.1 (lt_of_lt_of_le hp₀.1 hp₀.2) hp₁.1        (lt_of_lt_of_le hp₁.1 hp₁.2) hp₀p₁.ne hC₀ hC₁ hF) :    eLpNorm (T f) q ν ≤    ENNReal.ofReal (2 * A) * q ^ q⁻¹.toReal *    (((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ +    (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹)) ^ q⁻¹.toReal *    C₀ ^ (1 - t).toReal * C₁ ^ t.toReal * eLpNorm f p μ := by  have q_ne_zero : q ≠ 0 := (interpolated_pos' (lt_of_lt_of_le hp₀.1 hp₀.2)    (lt_of_lt_of_le hp₁.1 hp₁.2) (ne_top_of_Ioo ht) hq).ne'  have q_ne_top : q ≠ ⊤ := interp_exp_ne_top hq₀q₁ ht hq  have q'pos : 0 < q.toReal := toReal_pos q_ne_zero q_ne_top  refine le_of_rpow_le q'pos ?_  calc  _ = ∫⁻ x , ‖T f x‖ₑ ^ q.toReal ∂ν := by    unfold eLpNorm eLpNorm'    split_ifs <;> [contradiction; rw [one_div, ENNReal.rpow_inv_rpow q'pos.ne']]  _ ≤ _ := by    apply combine_estimates₀ (hT := hT) (p := p) <;> try assumption  _ = _ := by    repeat rw [ENNReal.mul_rpow_of_nonneg _ _ q'pos.le]    rw [ENNReal.ofReal_mul' q'pos.le]    repeat rw [ENNReal.rpow_mul]    congr    · rw [ofReal_rpow_of_nonneg] <;> positivity    · rw [toReal_inv, ENNReal.rpow_inv_rpow q'pos.ne']      exact ofReal_toReal_eq_iff.mpr q_ne_top    · rw [toReal_inv, ENNReal.rpow_inv_rpow q'pos.ne']