Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.combine_estimates₀

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:710 to 855

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 ν)
  (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)
  (h₁T : HasWeakType T p₁ q₁ μ ν C₁)
  (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
  (h₂T : PreservesAEStrongMeasurability T p (ν := ν) (μ := μ)) :
    ∫⁻ x , ‖T f x‖ₑ ^ q.toReal ∂ν ≤
    ENNReal.ofReal ((2 * A) ^ q.toReal * 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|⁻¹) *
    C₀ ^ ((1 - t).toReal * q.toReal) * C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal

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 ν)  (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)  (h₁T : HasWeakType T p₁ q₁ μ ν C₁)  (h₀T : HasWeakType T p₀ q₀ μ ν C₀)  (h₂T : PreservesAEStrongMeasurability T p (ν := ν) (μ := μ)) :    ∫⁻ x , ‖T f x‖ₑ ^ q.toReal ∂ν ≤    ENNReal.ofReal ((2 * A) ^ q.toReal * 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|⁻¹) *    C₀ ^ ((1 - t).toReal * q.toReal) * C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal := by  have one_le_p₀ := hp₀.1  have one_le_p1 := hp₁.1  have p₀pos : 0 < p₀ := hp₀.1  have q₀pos : 0 < q₀ := lt_of_lt_of_le hp₀.1 hp₀.2  have p₁pos : 0 < p₁ := hp₁.1  have q₁pos : 0 < q₁ := lt_of_lt_of_le hp₁.1 hp₁.2  have p_pos : 0 < p := interpolated_pos' one_le_p₀ one_le_p1 (ne_top_of_Ioo ht) hp  have : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support) :=    support_sigma_finite_from_MemLp hf (interp_exp_ne_top hp₀p₁.ne ht hp) p_pos.ne'  let tc := spf_to_tc spf  calc  ∫⁻ x , ‖T f x‖ₑ ^ q.toReal ∂ν    ≤ ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) * ∫⁻ s,      distribution (T (trunc f (tc.ton s))) s ν *      s^(q.toReal - 1) +      distribution (T (truncCompl f (tc.ton s))) s ν *      s^(q.toReal - 1) :=    estimate_norm_rpow_range_operator      (interp_exp_toReal_pos ht q₀pos q₁pos hq₀q₁ hq) _ hA hT (h₂T hf)  _ ≤ ENNReal.ofReal ((2 * A)^q.toReal * q.toReal) *      ((if q₁ < ⊤ then 1 else 0) * (C₁ ^ q₁.toReal * (∫⁻ s,        eLpNorm (trunc f (tc.ton s)) p₁ μ ^ q₁.toReal *        s ^ (q.toReal - q₁.toReal - 1))) +      (if q₀ < ⊤ then 1 else 0) * (C₀ ^ q₀.toReal * ∫⁻ s,        eLpNorm (truncCompl f (tc.ton s)) p₀ μ ^ q₀.toReal *        s ^ (q.toReal - q₀.toReal - 1))) := by    gcongr    apply estimate_norm_rpow_range_operator' (p := p) (tc := tc) p₀pos q₀pos q₁pos <;> try assumption    · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).2    · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).1    · intro q₀top s (hs : 0 < s)      apply weaktype_estimate_truncCompl_top (d := spf.d) hC₀ hp₀.1 q₀top _ _ hf h₀T hs _      · rw [hspf]        exact d_eq_top₀ one_le_p₀ q₁pos hp₀p₁.ne_top q₀top hq₀q₁      · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).1      · exact interp_exp_ne_top hp₀p₁.ne ht hp      · dsimp only [tc, spf_to_tc]        congr        rw [hspf]        dsimp only [spf_ch]        exact ζ_equality₇ ht one_le_p₀ q₀pos one_le_p1 q₁pos hp₀p₁.ne hq₀q₁ hp hq hp₀p₁.ne_top q₀top    · intro q₁top s (hs : 0 < s)      rcases (eq_or_ne p₁ ⊤) with p₁eq_top | p₁ne_top      · apply weaktype_estimate_trunc_top_top hC₁ _ p₁eq_top q₁top _ hf h₁T        · dsimp only [tc, spf_to_tc]          rw [hspf]          dsimp only [spf_ch]          rw [d_eq_top_top] <;> try assumption          rw [ζ_eq_top_top, ENNReal.rpow_one] <;> try assumption          exact hp₀p₁.ne        · exact p_pos        · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).2.le      · apply weaktype_estimate_trunc_top (p₁ := p₁) (p := p) (hd := spf.hd) hC₁ <;> try assumption        · unfold tc          rw [hspf]          dsimp only [spf_to_tc, spf_ch]          congr          apply ζ_equality₈ ht (hp₀p₁ := hp₀p₁.ne) <;> assumption        · rw [hspf]          dsimp only [spf_ch]          apply d_eq_top₁ <;> assumption        · exact p₁ne_top.lt_top        · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).2  _ ≤ ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) *      ((if q₁ < ⊤ then 1 else 0) * (C₁ ^ q₁.toReal *      ((spf.d ^ (q.toReal - q₁.toReal)) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ *        ((eLpNorm f p μ) ^ p.toReal) ^ ((sel ⊤ p₀ p₁).toReal ⁻¹ * (sel ⊤ q₀ q₁).toReal)))        +      (if q₀ < ⊤ then 1 else 0) * (C₀ ^ q₀.toReal *      ((spf.d ^ (q.toReal - q₀.toReal)) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ *        (((eLpNorm f p μ) ^ p.toReal) ^ ((sel ⊥ p₀ p₁).toReal ⁻¹ * (sel ⊥ q₀ q₁).toReal))))) := by      apply mul_le_mul_right      apply add_le_add      · split_ifs with is_q₁top        · gcongr          rw [lintegral_ennreal_eq_lintegral_Ioi_ofReal, ← lintegral_rw_aux power_aux_4]          apply estimate_trnc₁ (j := ⊤) ht <;> try assumption          · exact hp₁.2          · exact ne_top_of_Ioc hp₁ is_q₁top          · exact is_q₁top.ne_top          · exact hf.1          · rw [hspf]; rfl        · simp      · split_ifs with is_q₀top        · gcongr          rw [lintegral_ennreal_eq_lintegral_Ioi_ofReal, ← lintegral_rw_aux power_aux_4]          apply estimate_trnc₁ (j := ⊥) ht <;> try assumption          · exact hp₀.2          · exact ne_top_of_Ioc hp₀ is_q₀top          · exact is_q₀top.ne_top          · exact hf.1          · rw [hspf]; rfl        · simp  _ = (if q₁ < ⊤ then 1 else 0) *      (↑C₁ ^ q₁.toReal * (eLpNorm f p μ ^ p.toReal) ^ (q₁.toReal / p₁.toReal) *          spf.d ^ (q.toReal - q₁.toReal) * ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) *        ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹) +      (if q₀ < ⊤ then 1 else 0) *      (↑C₀ ^ q₀.toReal * (eLpNorm f p μ ^ p.toReal) ^ (q₀.toReal / p₀.toReal) *          spf.d ^ (q.toReal - q₀.toReal) * ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) *        ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) := by    dsimp only [sel]    ring_nf  _ = (if q₁ < ⊤ then 1 else 0) *      (↑C₀ ^ ((1 - t).toReal * q.toReal) * ↑C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal *          ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) *        ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹) +    (if q₀ < ⊤ then 1 else 0) *      (↑C₀ ^ ((1 - t).toReal * q.toReal) * ↑C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal *          ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) *        ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) := by    congr 1    · split_ifs with is_q₁top      · congr 3        apply simplify_factor₁ _ hp₀ <;> try assumption        · rw [hspf]; rfl        · exact is_q₁top.ne_top      · simp    · split_ifs with is_q₀top      · congr 3        apply simplify_factor₀ _ hp₀ hp₁ <;> try assumption        · rw [hspf]; rfl        · exact is_q₀top.ne_top      · simp  _ = _ := by split_ifs <;> ring