ComputationsChoiceExponent.ζ_eq_top_top

lemma ζ_eq_top_top (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 = 1 := by  rw [ζ_equality₂ ht, ← preservation_interpolation ht hp₀ hp₁ hp,    ← preservation_interpolation ht hq₀ hq₁ hq, hp₁', hq₁']  simp only [inv_top, toReal_zero, sub_zero]  rw [mul_comm, div_eq_mul_inv, mul_inv_cancel₀]  exact (mul_pos (interp_exp_inv_pos ht hq₀ hq₁ hq₀q₁ hq)    (interp_exp_inv_pos ht hp₀ hp₁ hp₀p₁ hp)).ne'