Source indexedlemma · leanprover/lean4:v4.32.0

ComputationsChoiceExponent.ζ_ne_zero

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:918 to 929

Mathematical statement

Exact Lean statement

lemma ζ_ne_zero (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₁) :
    ζ p₀ q₀ p₁ q₁ t.toReal ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ζ_ne_zero (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₁) :    ζ p₀ q₀ p₁ q₁ t.toReal ≠ 0 := by  refine div_ne_zero ?_ ?_  · apply mul_ne_zero (preservation_positivity_inv_toReal ht hp₀ hp₁ hp₀p₁).ne'    refine sub_ne_zero_of_ne (Ne.symm fun h ↦ hq₀q₁ ?_)    rw [← inv_inv q₀, ← inv_inv q₁, ← coe_inv_exponent hq₀, ← coe_inv_exponent hq₁]    exact congrArg Inv.inv (congrArg ENNReal.ofReal h)  · apply mul_ne_zero (preservation_positivity_inv_toReal ht hq₀ hq₁ hq₀q₁).ne'    refine sub_ne_zero_of_ne (Ne.symm fun h ↦ hp₀p₁ ?_)    rw [← inv_inv p₀, ← inv_inv p₁, ← coe_inv_exponent hp₀, ← coe_inv_exponent hp₁]    exact congrArg Inv.inv (congrArg ENNReal.ofReal h)