Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.simplify_factor₁

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:570 to 623

Mathematical statement

Exact Lean statement

lemma simplify_factor₁ {D : ℝ≥0∞}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (hq₁' : q₁ ≠ ⊤)
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁)
    (ht : t ∈ Ioo 0 1)
    (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
    (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤)
    (hD : D = @d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f) :
    C₁ ^ q₁.toReal * (eLpNorm f p μ ^ p.toReal) ^ (q₁.toReal / p₁.toReal) *
    (D ^ (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 simplify_factor₁ {D : ℝ≥0∞}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (hq₁' : q₁ ≠ ⊤)    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁)    (ht : t ∈ Ioo 0 1)    (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)    (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤)    (hD : D = @d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f) :    C₁ ^ q₁.toReal * (eLpNorm f p μ ^ p.toReal) ^ (q₁.toReal / p₁.toReal) *    (D ^ (q.toReal - q₁.toReal)) =    C₀ ^ ((1 - t).toReal * q.toReal) * C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal := by  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₁ne_top : p₁ ≠ ⊤ := ne_top_of_le_ne_top hq₁' hp₁.2  have hp' : p ∈ Ioo 0 ⊤ := interp_exp_in_Ioo_zero_top ht p₀pos p₁pos    (Decidable.not_or_of_imp fun _ ↦ p₁ne_top) hp  have p_toReal_pos : 0 < p.toReal := toReal_pos_of_Ioo hp'  rw [hD]  unfold d  nth_rw 2 [div_eq_mul_inv]  rw [ENNReal.mul_inv]  · repeat rw [ENNReal.mul_rpow_of_ne_zero _ _ (q.toReal - q₁.toReal)]    · rw [← ENNReal.rpow_neg, ← ENNReal.rpow_neg]      repeat rw [← ENNReal.rpow_mul]      repeat rw [← mul_assoc]      rw [simplify_factor_rw_aux₁ (a := C₁ ^ q₁.toReal)]      repeat rw [← ENNReal.rpow_add]      · rw [neg_mul]        congr 3        · rw [eq_exponents₆] <;> try assumption        · rw [eq_exponents₅] <;> try assumption        · rw [mul_assoc, mul_assoc, ← mul_add, eq_exponents₈, neg_mul,            eq_exponents₇ (ht := ht)] <;> try assumption          rw [← mul_add, ← add_mul, add_comm, ← preservation_interpolation ht hp₀.1 hp₁.1 hp,            toReal_inv]          field_simp      · exact ne_zero_of_Ioo hF      · exact ne_top_of_Ioo hF      · exact ne_zero_of_Ioo hF      · exact ne_top_of_Ioo hF      · exact (ENNReal.coe_pos.mpr hC₁).ne'      · exact coe_ne_top    · exact ENNReal.inv_ne_zero.mpr (by finiteness)    · exact ENNReal.inv_ne_zero.mpr (d_ne_top_aux₂ hF)    · positivity    · exact d_ne_zero_aux₀ hF    · exact d_ne_zero_aux₂ hC₀ hF    · exact mul_ne_zero (ENNReal.inv_ne_zero.mpr (by finiteness))        (ENNReal.inv_ne_zero.mpr (d_ne_top_aux₂ hF))  · exact Or.inr (d_ne_top_aux₂ hF)  · exact Or.inr (d_ne_zero_aux₀ hF)