Source indexedlemma · leanprover/lean4:v4.32.0

ComputationsChoiceExponent.ζ_equality₂

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:556 to 568

Mathematical statement

Exact Lean statement

lemma ζ_equality₂ (ht : t ∈ Ioo 0 1) :
    ζ p₀ q₀ p₁ q₁ t.toReal =
    (((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal) *
    ((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal - q₁⁻¹.toReal)) /
    (((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal) *
    ((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal - p₁⁻¹.toReal))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ζ_equality₂ (ht : t ∈ Ioo 0 1) :    ζ p₀ q₀ p₁ q₁ t.toReal =    (((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal) *    ((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal - q₁⁻¹.toReal)) /    (((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal) *    ((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal - p₁⁻¹.toReal)) := by  unfold ζ  have : -(1 - t.toReal) < 0 := by    rw [neg_neg_iff_pos, sub_pos, ← toReal_one]    exact toReal_strict_mono one_ne_top ht.2  rw [← mul_div_mul_right _ _ this.ne, mul_assoc _ _ (-(1 - t.toReal)),    mul_assoc _ _ (-(1 - t.toReal)), ← sub_toReal_of_le ht.2.le]  congr <;> ring