Source indexedlemma · leanprover/lean4:v4.32.0

ComputationsChoiceExponent.ζ_equality₄

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:611 to 622

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ζ_equality₄ (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁)    (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤)    (hq₁' : q₁ ≠ ⊤) :    ζ p₀ q₀ p₁ q₁ t.toReal =    (p₁.toReal * (q₁.toReal - q.toReal)) / (q₁.toReal * (p₁.toReal - p.toReal)) := by  rw [ζ_symm, ζ_equality₃ (mem_sub_Ioo one_ne_top ht)] <;> try assumption  · exact hp₀p₁.symm  · exact hq₀q₁.symm  · rw [hp, add_comm, ENNReal.sub_sub_cancel one_ne_top ht.2.le]  · rw [hq, add_comm, ENNReal.sub_sub_cancel one_ne_top ht.2.le]