Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.simplify_factor₀

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:515 to 568

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 (by left; exact 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] <;> try positivity      · congr 1        · congr 1          · rw [eq_exponents₀] <;> try assumption          · rw [neg_mul, eq_exponents₁ (t := t)] <;> try assumption            ring_nf        · congr 1          rw [mul_assoc, ← mul_add, eq_exponents₂ (t := t)] <;> try assumption          rw [mul_assoc, mul_assoc, ← mul_add, neg_mul, eq_exponents₃ (t := t)] <;> try assumption          simp only [neg_mul, neg_neg]          rw [← mul_assoc, ← add_mul, ← 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 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)