Source indexedlemma · leanprover/lean4:v4.32.0

ComputationsChoiceExponent.eq_exponents₇

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:1075 to 1086

Mathematical statement

Exact Lean statement

lemma eq_exponents₇ (ht : t ∈ Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁)
    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) :
    q₁.toReal / p₁.toReal + -(p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) *
    (q.toReal - q₁.toReal)) =
    t.toReal * p₁⁻¹.toReal * q.toReal

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eq_exponents₇ (ht : t ∈ Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁)    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) :    q₁.toReal / p₁.toReal + -(p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) *    (q.toReal - q₁.toReal)) =    t.toReal * p₁⁻¹.toReal * q.toReal := by  rw [div_eq_mul_inv, toReal_inv]  calc  _ = p₁.toReal⁻¹ * (q₁.toReal + - (q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) *      (q.toReal - q₁.toReal))) := by ring  _ = _ := by    rw [eq_exponents₅ (ht := ht)] <;> try assumption    ring