fpvandoorn/carleson
Source indexedlemma · leanprover/lean4:v4.32.0
ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₀
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:931 to 940
Mathematical statement
Exact Lean statement
lemma ζ_le_zero_iff_of_lt₀ (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁)
(hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :
ζ p₀ q₀ p₁ q₁ t.toReal ≤ 0 ↔ q < q₀Complete declaration
Lean source
Full Lean sourceLean 4
lemma ζ_le_zero_iff_of_lt₀ (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : ζ p₀ q₀ p₁ q₁ t.toReal ≤ 0 ↔ q < q₀ := by constructor <;> intro h · rcases (Decidable.lt_or_eq_of_le h) with ζ_lt_0 | ζ_eq_0 · exact (ζ_neg_iff_of_lt₀ ht hp₀ hq₀ hp₁ hq₁ hq₀q₁ hp hq hp₀p₁').mp ζ_lt_0 · exact False.elim <| (ζ_ne_zero ht hp₀ hq₀ hp₁ hq₁ hp₀p₁'.ne hq₀q₁) ζ_eq_0 · exact ((ζ_neg_iff_of_lt₀ ht hp₀ hq₀ hp₁ hq₁ hq₀q₁ hp hq hp₀p₁').mpr h).le