fpvandoorn/carleson
Source indexedlemma · leanprover/lean4:v4.32.0
MeasureTheory.estimate_trnc₁
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:697 to 809
Source documentation
One of the key estimates for the real interpolation theorem, now using
the particular choice of exponent, but not yet using the
particular choice of scale in the ScaledPowerFunction.
Exact Lean statement
lemma estimate_trnc₁ {spf : ScaledPowerFunction} {j : Bool}
[TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (ht : t ∈ Ioo 0 1)
(hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hpq : sel j p₀ p₁ ≤ sel j q₀ q₁)
(hp' : sel j p₀ p₁ ≠ ⊤) (hq' : sel j q₀ q₁ ≠ ⊤) (hp₀p₁ : p₀ < p₁)
(hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hf : AEStronglyMeasurable f μ) (hf₂ : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support))
(hspf : spf.σ = ζ p₀ q₀ p₁ q₁ t.toReal) :
∫⁻ s : ℝ in Ioi 0,
eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (sel j p₀ p₁) μ ^ (sel j q₀ q₁).toReal *
ENNReal.ofReal (s ^ (q.toReal - (sel j q₀ q₁).toReal - 1)) ≤
(spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) *
ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ *
((eLpNorm f p μ) ^ p.toReal) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal)Complete declaration
Lean source
Full Lean sourceLean 4
lemma estimate_trnc₁ {spf : ScaledPowerFunction} {j : Bool} [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hpq : sel j p₀ p₁ ≤ sel j q₀ q₁) (hp' : sel j p₀ p₁ ≠ ⊤) (hq' : sel j q₀ q₁ ≠ ⊤) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hf : AEStronglyMeasurable f μ) (hf₂ : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support)) (hspf : spf.σ = ζ p₀ q₀ p₁ q₁ t.toReal) : ∫⁻ s : ℝ in Ioi 0, eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (sel j p₀ p₁) μ ^ (sel j q₀ q₁).toReal * ENNReal.ofReal (s ^ (q.toReal - (sel j q₀ q₁).toReal - 1)) ≤ (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * ((eLpNorm f p μ) ^ p.toReal) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by have p_toReal_pos : 0 < p.toReal := interp_exp_toReal_pos' ht hp₀ hp₁ hp (Or.inl hp₀p₁.ne_top) have simpl_exp : (sel j p₀ p₁).toReal + spf.σ⁻¹ * (q.toReal - (sel j q₀ q₁).toReal) * ((sel j p₀ p₁).toReal / (sel j q₀ q₁).toReal) = p.toReal := by rcases j · dsimp only [sel] rw [hspf] apply ζ_equality₅ (hp₀p₁ := hp₀p₁.ne) <;> assumption · dsimp only [sel] rw [hspf] apply ζ_equality₆ (hp₀p₁ := hp₀p₁.ne) <;> assumption have : 0 < (sel j q₀ q₁).toReal := by apply toReal_pos _ hq' rcases j · exact hq₀.ne' · exact hq₁.ne' have : 0 < (sel j p₀ p₁).toReal := by apply toReal_pos _ hp' rcases j · exact hp₀.ne' · exact hp₁.ne' calc _ ≤ (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support, ‖f a‖ₑ ^ ((sel j p₀ p₁).toReal + spf.σ⁻¹ * (q.toReal - (sel j q₀ q₁).toReal) * ((sel j p₀ p₁).toReal / (sel j q₀ q₁).toReal)) ∂μ) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by have coe_p' : ENNReal.ofReal (sel j p₀ p₁).toReal = (sel j p₀ p₁) := ofReal_toReal_eq_iff.mpr hp' nth_rw 1 [← coe_p'] apply estimate_trnc · apply toReal_pos · cases j · exact hp₀.ne' · exact hp₁.ne' · exact hp' · apply toReal_pos · cases j · exact hq₀.ne' · exact hq₁.ne' · exact hq' · exact toReal_mono hq' hpq · exact hf · exact hf₂ · unfold spf_to_tc cases j · unfold sel dsimp only simp only [hspf, Bool.if_false_right, Bool.and_true, Bool.false_bne, decide_eq_true_eq] split_ifs with is_ζ_pos · apply toReal_strict_mono · exact interp_exp_ne_top hq₀q₁ ht hq · exact (ζ_pos_iff_of_lt₀ ht hp₀ hq₀ hp₁ hq₁ hq₀q₁ hp hq hp₀p₁).mp is_ζ_pos · apply toReal_strict_mono hq' exact (ζ_le_zero_iff_of_lt₀ ht hp₀ hq₀ hp₁ hq₁ hq₀q₁ hp hq hp₀p₁).mp (le_of_not_gt is_ζ_pos) · unfold sel dsimp only simp only [hspf, Bool.if_false_right, Bool.and_true, Bool.true_bne, Bool.not_eq_true', decide_eq_false_iff_not] split_ifs with is_ζ_pos · apply toReal_strict_mono hq' exact (ζ_pos_iff_of_lt₁ ht hp₀ hq₀ hp₁ hq₁ hq₀q₁ hp hq hp₀p₁).mp is_ζ_pos · apply toReal_strict_mono · exact interp_exp_ne_top hq₀q₁ ht hq · exact (ζ_le_zero_iff_of_lt₁ ht hp₀ hq₀ hp₁ hq₁ hq₀q₁ hp hq hp₀p₁).mp (le_of_not_gt is_ζ_pos) · have : 0 < (sel j p₀ p₁).toReal / (sel j q₀ q₁).toReal := by positivity refine (pos_iff_pos_of_mul_pos ?_).mpr this rw [add_mul, ← mul_div_assoc, mul_div_cancel_left₀, simpl_exp] <;> positivity _ = (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support, (‖f a‖ₑ ^ p.toReal) ∂μ) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by congr ext x congr _ ≤ (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by gcongr exact Measure.restrict_le_self _ = (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * (((∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ) ^ p.toReal) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by congr rw [ENNReal.rpow_inv_rpow] positivity _ = (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * ((eLpNorm f p μ) ^ p.toReal) ^ ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by congr rw [← one_div] refine (eLpNorm_eq_lintegral_rpow_enorm_toReal (ε := E₁) ?_ ?_).symm · exact (interpolated_pos' hp₀ hp₁ (ne_top_of_Ioo ht) hp).ne' · exact interp_exp_ne_top hp₀p₁.ne ht hp