diff --git a/Mathlib.lean b/Mathlib.lean index a861355e4f0c01..75e92359ad0143 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5522,6 +5522,10 @@ public import Mathlib.NumberTheory.SmoothNumbers public import Mathlib.NumberTheory.SumFourSquares public import Mathlib.NumberTheory.SumPrimeReciprocals public import Mathlib.NumberTheory.SumTwoSquares +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlg +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlgSetup +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAnalytic +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainOrder public import Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart public import Mathlib.NumberTheory.Transcendental.Liouville.Basic public import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber diff --git a/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAlg.lean b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAlg.lean new file mode 100644 index 00000000000000..bf246027794bb9 --- /dev/null +++ b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAlg.lean @@ -0,0 +1,415 @@ +/- +Copyright (c) 2026 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ + +module + +public import Mathlib.Analysis.Complex.Basic +public import Mathlib.NumberTheory.NumberField.House + +/-! +# Hilbert's Seventh Problem (Gelfond–Schneider Theorem) +The goal of this file is to formalize a proof of the **Gelfond–Schneider Theorem**, which solves +Hilbert’s Seventh Problem: namely, that for algebraic numbers `α ≠ 0, 1` and irrational algebraic +`β`, the number `α ^ β` is transcendental. + +## Main results +* `gelfondSchneider`: If `α` and `β` are algebraic, `α ≠ 0`, `α ≠ 1`, and `β` is irrational, then + `α ^ β` is transcendental. + +## Implementation details +We follow the proof in Keng’s *Introduction to Number Theory*, Chapter 17, Section 5, p.488 - 493. + +The argument proceeds by contradiction. The core of the proof is an auxiliary function lemma, where +we construct a nonzero integer linear combination of exponential functions that vanishes to high +order at several algebraic points. + +This specific file handles the foundational algebraic setup: +1. Constructing a common number field `K` of degree `h` containing `α, β, γ`. +2. Defining the structural parameters `m = 2h + 2` and `n = q^2 / (2m)`. +3. Establishing the common denominator scaling factor `c₁` such that `c₁α`, `c₁β`, and `c₁γ` + are all algebraic integers in `K`. +4. Formulating the homogeneous linear system matrix `A` with scaled entries residing strictly + in the ring of integers `𝓞 K`, ready for Siegel's Lemma. + +## References +Loo-Keng Hua, Introduction to Number Theory, Springer, 1982. Chapter XII (§13). +A. O. Gelfond (1934), *Sur le septième Problème de Hilbert +T. Schneider (1935), *Transzendenzuntersuchungen periodischer Funktionen* +-/ + +@[expose] public section + +open BigOperators Module.Free Fintype NumberField Embeddings FiniteDimensional + Matrix Set Polynomial Finset IntermediateField Complex AnalyticAt + +noncomputable section + +/-! +Suppose that `α, β, γ` lie in an algebraic field `K` with degree `h`. +-/ + +lemma isNumberField_adjoin_of_isAlgebraic (α β γ : ℂ) (hα : IsAlgebraic ℚ α) (hβ : IsAlgebraic ℚ β) + (hγ : IsAlgebraic ℚ γ) : NumberField (adjoin ℚ {α, β, γ}) where + to_charZero := charZero_of_injective_algebraMap (algebraMap ℚ _).injective + to_finiteDimensional := finiteDimensional_adjoin fun _ hx ↦ by + rcases hx with rfl | rfl | rfl + exacts [isAlgebraic_iff_isIntegral.1 hα, isAlgebraic_iff_isIntegral.1 hβ, + isAlgebraic_iff_isIntegral.1 hγ] + +lemma exists_common_field_of_isAlgebraic (α β γ : ℂ) (hα : IsAlgebraic ℚ α) (hβ : IsAlgebraic ℚ β) + (hγ : IsAlgebraic ℚ γ) : ∃ (K : Type) (_ : Field K) (_ : NumberField K) (σ : K →+* ℂ) + (_ : DecidableEq (K →+* ℂ)), ∃ (α' β' γ' : K), α = σ α' ∧ β = σ β' ∧ γ = σ γ' := by + refine ⟨adjoin ℚ {α, β, γ}, ?_⟩ + let σ : ↥(adjoin ℚ {α, β, γ}) →+* ℂ := + { toFun := fun x ↦ x.1, map_one' := rfl, map_mul' := fun _ _ ↦ rfl, + map_zero' := rfl, map_add' := fun _ _ ↦ rfl } + refine ⟨inferInstance, isNumberField_adjoin_of_isAlgebraic α β γ hα hβ hγ, σ, + Classical.typeDecidableEq _, ⟨⟨α, ?_⟩, ⟨β, ?_⟩, ⟨γ, ?_⟩, ?_⟩⟩ + · apply subset_adjoin + simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or] + · apply subset_adjoin + simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true] + · apply subset_adjoin + simp only [Set.mem_insert_iff, Set.mem_singleton_iff, or_true] + · dsimp [σ] + exact ⟨rfl, ⟨rfl, rfl⟩⟩ + +variable {K} [Field K] [NumberField K] + +lemma exists_int_smul_isIntegral {K : Type*} [Field K] [NumberField K] (α : K) : + ∃ k : ℤ, k ≠ 0 ∧ IsIntegral ℤ (k • α) := by + obtain ⟨y, hy, hf⟩ := exists_integral_multiples ℤ ℚ (L := K) {α} + refine ⟨y, hy, hf α (mem_singleton_self _)⟩ + +/-- A choice of a non-zero integer `c` such that `c • α` is an algebraic integer. +The existence of such an integer is guaranteed for any algebraic number. -/ +def c₀ {K : Type*} [Field K] [NumberField K] (α : K) : {c : ℤ // c ≠ 0 ∧ IsIntegral ℤ (c • α)} := + ⟨(exists_int_smul_isIntegral α).choose, (exists_int_smul_isIntegral α).choose_spec⟩ + +/-- An abbreviation for the explicit integer value extracted from `c₀ α`. -/ +abbrev c₀Coeff {K : Type*} [Field K] [NumberField K] (α : K) : ℤ := (c₀ α : ℤ) + +lemma c₀Coeff_ne_zero (α : K) : c₀Coeff α ≠ 0 := (c₀ α).2.1 + +/-! +Let `α` and `β` be algebraic numbers with `α ≠ 0, 1` and `β` irrational. We prove that `αᵇ` is +transcendental by contradiction. Suppose `γ = αᵇ = e^(β log α)` is also algebraic. +-/ + +/-- This structure encapsulates all the foundational data and hypotheses for the proof +of the Gelfond-Schneider theorem. It binds the complex numbers to their algebraic +counterparts in a common number field. -/ +structure Setup where + /-- The base of the exponentiation, assumed to be an algebraic complex number. -/ + α : ℂ + /-- The exponent, assumed to be an irrational algebraic complex number. -/ + β : ℂ + /-- A common abstract type representing the number field containing the preimages + of `α`, `β`, and `α ^ β`. -/ + K : Type + [isField : Field K] + [isNumberField : NumberField K] + /-- A fixed ring homomorphism embedding the abstract number field `K` into `ℂ`. -/ + σ : K →+* ℂ + /-- The algebraic preimage of `α` in the number field `K`. -/ + α' : K + /-- The algebraic preimage of `β` in the number field `K`. -/ + β' : K + /-- The algebraic preimage of the assumed-algebraic `α ^ β` in the number field `K`. -/ + γ' : K + hirr : ∀ i j : ℤ, β ≠ i / j + htriv : α ≠ 0 ∧ α ≠ 1 + hα : IsAlgebraic ℚ α + hβ : IsAlgebraic ℚ β + habc : α = σ α' ∧ β = σ β' ∧ α ^ β = σ γ' + /-- A decidable equality instance for the complex embeddings of `K`. -/ + hd : DecidableEq (K →+* ℂ) + +namespace Setup + +attribute [instance] isField isNumberField + +variable (h7 : Setup) + +open Setup + +lemma alpha_gamma_pow_beta_ne_zero : h7.α ^ h7.β ≠ 0 := + fun H ↦ h7.htriv.1 ((cpow_eq_zero_iff h7.α h7.β).mp H).1 + +lemma beta_ne_zero : h7.β ≠ 0 := + fun H ↦ h7.hirr 0 1 (by simpa [div_one] using H) + +lemma alpha'_beta'_gamma'_ne_zero : h7.α' ≠ 0 ∧ h7.β' ≠ 0 ∧ h7.γ' ≠ 0 := by + refine ⟨?_, ?_, ?_⟩ <;> intro H + · exact h7.htriv.1 (by simp [h7.habc.1, H, map_zero h7.σ]) + · exact h7.beta_ne_zero (by simp [h7.habc.2.1, H, map_zero h7.σ]) + · exact h7.alpha_gamma_pow_beta_ne_zero (by simp [h7.habc.2.2, H, map_zero h7.σ]) + +lemma alpha'_ne_one : h7.α' ≠ 1 := fun h ↦ + h7.htriv.2 <| by simpa [h7.habc.1, map_one] using congrArg h7.σ h + +lemma beta'_ne_zero : h7.β' ≠ 0 := h7.alpha'_beta'_gamma'_ne_zero.2.1 + +open Complex + +lemma log_α_ne_zero : log h7.α ≠ 0 := + mt (fun h ↦ by simpa [exp_log h7.htriv.1, exp_zero] using congrArg exp h) h7.htriv.2 + +/-- c₁ is a positive integer such that c₁ • α', c₁ • β', c₁ • γ' are algebraic integers -/ +def c₁ : ℤ := abs (c₀ h7.α' * c₀ h7.β' * c₀ h7.γ') + +lemma one_le_c₁ : 1 ≤ h7.c₁ := by + simpa [c₁] using Int.one_le_abs <| mul_ne_zero (mul_ne_zero (c₀Coeff_ne_zero h7.α') + (c₀Coeff_ne_zero h7.β')) (c₀Coeff_ne_zero h7.γ') + +lemma one_le_abs_c₁ : 1 ≤ |↑h7.c₁| := Int.one_le_abs (Ne.symm (Int.ne_of_lt h7.one_le_c₁)) + +lemma IsIntegral_assoc (K : Type) [Field K] {x y : ℤ} (z : ℤ) (α : K) (ha : IsIntegral ℤ (z • α)) : + IsIntegral ℤ ((x * y * z : ℤ) • α) := by + simpa [Int.cast_mul, zsmul_eq_mul, mul_assoc] using IsIntegral.smul (x * y) ha + +lemma isIntegral_c₁α : IsIntegral ℤ (h7.c₁ • h7.α') := by + have h := IsIntegral_assoc (x := c₀Coeff h7.γ') (y := c₀Coeff h7.β') h7.K (c₀Coeff h7.α') h7.α' + ((c₀ h7.α').2.2) + conv => enter [2]; rw [c₁, mul_comm, mul_comm (c₀Coeff h7.α') (c₀Coeff h7.β'), ← mul_assoc] + rcases abs_choice (c₀Coeff h7.γ' * c₀Coeff h7.β' * c₀Coeff h7.α') with H1 | H2 + · rw [H1]; exact h + · rw [H2]; rw [← IsIntegral.neg_iff, neg_smul, neg_neg]; exact h + +lemma isIntegral_c₁β : IsIntegral ℤ (h7.c₁ • h7.β') := by + have h := IsIntegral_assoc (x := c₀Coeff h7.γ') (y := c₀Coeff h7.α') h7.K (c₀Coeff h7.β') h7.β' + ((c₀ h7.β').2.2) + rw [c₁, mul_comm, ← mul_assoc] + rcases abs_choice (c₀Coeff h7.γ' * c₀Coeff h7.α' * c₀Coeff h7.β') with H1 | H2 + · rw [H1]; exact h + · rw [H2]; rw [← IsIntegral.neg_iff, neg_smul, neg_neg]; exact h + +lemma isIntegral_c₁γ : IsIntegral ℤ (h7.c₁ • h7.γ') := by + have h := IsIntegral_assoc (x := c₀Coeff h7.α') (y := c₀Coeff h7.β') h7.K (c₀Coeff h7.γ') h7.γ' + ((c₀ h7.γ').2.2) + rw [c₁] + rcases abs_choice (c₀Coeff h7.α' * c₀Coeff h7.β' * c₀Coeff h7.γ') with H1 | H2 + · rw [H1]; exact h + · rw [H2]; rw [← IsIntegral.neg_iff, neg_smul, neg_neg]; exact h + +/-! +Let `m = 2h + 2`, and `n = q^ 2 / (2 * h7.m)`, where $q^2 = t $ is a square of a natural number +and is a multiple of $2m.$ -/ + +/-- The finrank of the field extension `h7.K` -/ +def h : ℕ := Module.finrank ℚ h7.K + +/-- A parameter `m` dependent on the degree `h = [K : ℚ]`. -/ +def m : ℕ := 2 * h7.h + 2 + +lemma one_le_m : 1 ≤ h7.m := Nat.succ_le_succ (Nat.zero_le (2 * h7.h + 1)) + +variable (q : ℕ) (hq0 : 0 < q) + +/-- A target bound parameter `n` dependent on a free parameter `q`. -/ +def n : ℕ := q ^ 2 / (2 * h7.m) + +variable (u : Fin (h7.m * h7.n q)) (t : Fin (q * q)) + +-- `a, b, k, l` are values that depend on the context variables `t` and `u`. + +/-- A variable `a` that satisfies `1 ≤ a ≤ q`. -/ +def a : ℕ := (finProdFinEquiv.symm.toFun t).1 + 1 + +/-- A variable `b` that satisfies `1 ≤ b ≤ q`. -/ +def b : ℕ := (finProdFinEquiv.symm.toFun t).2 + 1 + +/-- Also, let `ρ₁, ρ₂, …, ρₜ` represent the `t` numbers + `(a + bβ) log α, 1 ≤ a ≤ q, 1 ≤ b ≤ q.` -/ +def ρ : ℂ := (a q t + (b q t • h7.β)) * Complex.log h7.α + +/-! +We introduce the integral function + `R(x) = η₁ e^(ρ₁ x) + … + ηₜ e^(ρₜ x)` +where the coefficients `η₁, …, ηₜ` are determined by the following conditions. +The function `R` is defined in the next file. + +We solve the system of `mn` homogeneous linear equations + `(log α)⁻ᵏ R⁽ᵏ⁾(l) = 0, 0 ≤ k ≤ n - 1, 1 ≤ l ≤ m` +in the `t = 2mn` unknowns `η₁, …, ηₜ`. It follows from +`house.exists_ne_zero_int_vec_house_le` that there is a non-trivial set of integer +solutions `η₁, …, η₂` in `K`. +-/ + +/-! +The coefficients are in `K` and + `(log α)⁻ᵏ ((a + bβ) log α)ᵏ e^(l(a + bβ) log α) = (a + bβ)ᵏ αᵃˡ γᵇˡ` +for `1 ≤ l ≤ m, 1 ≤ a, b ≤ q, 0 ≤ k ≤ n - 1`.-/ + +/-- A variable `k` that satisfies 0 ≤ k ≤ n - 1 -/ +def k : ℕ := (finProdFinEquiv.symm.toFun u).2 + +/-- A variable `l` that satisfies 1 ≤ l ≤ m -/ +def l : ℕ := (finProdFinEquiv.symm.toFun u).1 + 1 + +/-- The core algebraic coefficient appearing in the evaluation of the `k`-th derivative +of the auxiliary function at point `l`. Evaluates to `(a + bβ')^k * α'^(al) * γ'^(bl)`. -/ +abbrev systemCoeffs : h7.K := + (a q t + b q t • h7.β') ^ (h7.k q u) * h7.α' ^ (a q t * h7.l q u) * h7.γ' ^ (b q t * h7.l q u) + +variable (h2mq : 2 * h7.m ∣ q ^ 2) + +include hq0 h2mq in +lemma one_le_n : 1 ≤ h7.n q := by + simp [n, (Nat.one_le_div_iff (by positivity [h7.one_le_m])).2 + (Nat.le_of_dvd (Nat.pow_pos hq0) h2mq)] + +/-! +Let `c₁, c₂, …` be natural numbers independent of `n`. There exists `c₁` such that +`c₁ α, c₁ β, c₁ γ` are integers in `K`. +-/ + +/-- A combined integer scaling factor `c₁^(n-1 + 2mq)` applied to the linear system to clear +all denominators and ensure the resulting matrix entries are algebraic integers. -/ +abbrev c_coeffs (q : ℕ) := h7.c₁ ^ (h7.n q - 1) * h7.c₁ ^ (h7.m * q) * h7.c₁ ^ (h7.m * q) + +/-- An unscaled sub-component of the matrix coefficients, used to establish intermediate +integrality bounds during the construction of the auxiliary function. -/ +abbrev c_coeffs0 (q : ℕ) (u : Fin (h7.m * h7.n q)) (t : Fin (q * q)) := + h7.c₁ ^ (h7.k q u : ℕ) * h7.c₁ ^ (a q t * h7.l q u) * h7.c₁ ^ (b q t * h7.l q u) + +lemma IsIntegral.Cast (K : Type) [Field K] (a : ℤ) : IsIntegral ℤ (a : K) := + map_isIntegral_int (algebraMap ℤ K) (Algebra.IsIntegral.isIntegral _) + +lemma isIntegral_c₁_pow_smul_pow (u : h7.K) (n k a l : ℕ) (hnk : a * l ≤ n * k) + (H : IsIntegral ℤ (↑h7.c₁ * u)) : IsIntegral ℤ (h7.c₁ ^ (n * k) • u ^ (a * l)) := by + rw [zsmul_eq_mul, Int.cast_pow, ← Nat.sub_add_cancel hnk, pow_add, mul_assoc, ← mul_pow] + exact IsIntegral.mul (IsIntegral.pow (IsIntegral.Cast h7.K h7.c₁) _) (IsIntegral.pow H _) + +lemma IsIntegral.Nat (K : Type) [Field K] (a : ℕ) : IsIntegral ℤ (a : K) := by + have : (a : K) = ((a : ℤ) : K) := by simp only [Int.cast_natCast] + rw [this]; apply IsIntegral.Cast + +lemma isIntegral_c₁_pow_smul_α'_pow : IsIntegral ℤ + (h7.c₁ ^ (a q t * h7.l q u) • (h7.α' ^ (a q t * h7.l q u))) := by + apply h7.isIntegral_c₁_pow_smul_pow h7.α' (a q t) (h7.l q u) (a q t) (h7.l q u) (by rfl) + (by grind [h7.isIntegral_c₁α]) + +lemma isIntegral_c₁_pow_smul_γ'_pow : IsIntegral ℤ (h7.c₁ ^ (b q t * h7.l q u) • + (h7.γ'^ (b q t * (h7.l q u)))) := by + apply h7.isIntegral_c₁_pow_smul_pow h7.γ' (b q t) (h7.l q u) (b q t) (h7.l q u) (by rfl) + (by grind [h7.isIntegral_c₁γ]) + +lemma isIntegral_c₁_pow_smul_α'_pow' : + IsIntegral ℤ (h7.c₁^(h7.m * q) • (h7.α' ^ (a q t * h7.l q u))) := + h7.isIntegral_c₁_pow_smul_pow h7.α' h7.m q (a q t) (h7.l q u) + (by simpa [mul_comm] using Nat.mul_le_mul (((finProdFinEquiv.symm.toFun t).1).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt)) <| by grind [h7.isIntegral_c₁α] + +lemma isIntegral_c₁_pow_smul_γ'_pow' : + IsIntegral ℤ (h7.c₁ ^ (h7.m * q) • (h7.γ'^ (b q t * h7.l q u))) := + h7.isIntegral_c₁_pow_smul_pow h7.γ' h7.m q (b q t) (h7.l q u) + (by simpa [mul_comm] using Nat.mul_le_mul (((finProdFinEquiv.symm.toFun t).2).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt)) <| by grind [h7.isIntegral_c₁γ] + +lemma c_coeffs_neq_zero : h7.c_coeffs q ≠ 0 := + mul_ne_zero (mul_ne_zero (pow_ne_zero _ (Ne.symm (Int.ne_of_lt h7.one_le_c₁))) + (pow_ne_zero _ (Ne.symm (Int.ne_of_lt h7.one_le_c₁)))) + (pow_ne_zero _ (Ne.symm (Int.ne_of_lt h7.one_le_c₁))) + +lemma isIntegral_c₁_pow_smul_add_smul_pow (n : ℕ) (k : ℕ) (hkn : k ≤ n - 1) (a : ℕ) (b : ℕ) : + IsIntegral ℤ (h7.c₁ ^ (n - 1) • (↑a + ↑b • h7.β') ^ k) := by + rw [zsmul_eq_mul, Int.cast_pow, ← Nat.sub_add_cancel hkn, pow_add, mul_assoc, ← mul_pow, mul_add] + refine IsIntegral.mul (IsIntegral.pow (IsIntegral.Cast _ _) _) + (IsIntegral.pow (IsIntegral.add ?_ ?_) _) + · exact IsIntegral.mul (IsIntegral.Cast _ _) (IsIntegral.Nat _ _) + · rw [nsmul_eq_mul, ← mul_assoc, mul_comm (h7.c₁ : h7.K), mul_assoc] + exact IsIntegral.mul (IsIntegral.Nat _ _) (by grind [h7.isIntegral_c₁β]) + +/-! +Multiplying the system by +`c₁^(n-1) c₁^(mq) c₁^ (mq) = c₁^(n-1+2mq) ≤ (c₂^n)` ensures the coefficients are integers in `K`. -/ + +lemma zsmul_mul_mul_distrib {K : Type*} [Field K] (a b c : ℤ) (x y z : K) : + ((a * b) * c) • ((x * y) * z) = a • x * b • y * c • z := by + simp [zsmul_eq_mul]; ring + +open Nat in +lemma c₁IsInt : IsIntegral ℤ (h7.c_coeffs q • h7.systemCoeffs q u t) := by + rw [zsmul_mul_mul_distrib, mul_assoc] + refine IsIntegral.mul ?_ + (IsIntegral.mul (h7.isIntegral_c₁_pow_smul_α'_pow' q u t) + (h7.isIntegral_c₁_pow_smul_γ'_pow' q u t)) + · exact h7.isIntegral_c₁_pow_smul_add_smul_pow (h7.n q) (h7.k q u) + (le_sub_one_of_lt (finProdFinEquiv.symm.1 u).2.isLt) (a q t) (b q t) + +/-- The matrix representing the homogeneous linear system of `mn` equations in `q^2` unknowns. +Its entries are scaled to strictly reside in the ring of integers `𝓞 K`. -/ +def A : Matrix (Fin (h7.m * h7.n q)) (Fin (q * q)) (𝓞 h7.K) := + fun i j ↦ RingOfIntegers.restrict _ (fun _ ↦ (h7.c₁IsInt q i j)) ℤ + +lemma c₁_ne_zero : h7.c₁ ≠ 0 := Ne.symm (Int.ne_of_lt h7.one_le_c₁) + +lemma c₁α_ne_zero : h7.c₁ • h7.α' ≠ 0 := by + simpa using ⟨Ne.symm (Int.ne_of_lt h7.one_le_c₁), (h7.alpha'_beta'_gamma'_ne_zero).1⟩ + +lemma c₁γ_ne_zero : h7.c₁ • h7.γ' ≠ 0 := by + simpa using ⟨Ne.symm (Int.ne_of_lt h7.one_le_c₁), (h7.alpha'_beta'_gamma'_ne_zero).2.2⟩ + +lemma house_bound_c₁α : + house (h7.c₁ • h7.α') ^ (a q t * h7.l q u) ≤ house (h7.c₁ • h7.α') ^ (h7.m * q) := by + refine Bound.pow_le_pow_right_of_le_one_or_one_le (Or.inl ⟨one_le_house_of_isIntegral + (h7.isIntegral_c₁α) h7.c₁α_ne_zero, ?_⟩) + simpa [mul_comm] using mul_le_mul (((finProdFinEquiv.symm.toFun t).1).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt) (zero_le _) (zero_le _) + +lemma isInt_β_bound : IsIntegral ℤ (h7.c₁ • (↑q + q • h7.β')) := by + simpa [smul_add, zsmul_eq_mul, nsmul_eq_mul, mul_assoc, mul_left_comm, mul_comm] using + (IsIntegral.add ((IsIntegral.Cast h7.K h7.c₁).mul (IsIntegral.Nat h7.K q)) + ((IsIntegral.Nat h7.K q).mul h7.isIntegral_c₁β)) + +lemma isInt_β_bound_low (q : ℕ) (t : Fin (q * q)) : + IsIntegral ℤ (h7.c₁ • (↑(a q t) + b q t • h7.β')) := by + simpa [smul_add, zsmul_eq_mul, nsmul_eq_mul, mul_add, + mul_assoc, mul_comm, mul_left_comm, add_assoc, add_comm, add_left_comm] using + (IsIntegral.add + ((IsIntegral.Cast h7.K h7.c₁).mul (IsIntegral.Nat h7.K (a q t))) + ((IsIntegral.Nat h7.K (b q t)).mul h7.isIntegral_c₁β)) + +lemma β'_ne_zero (y : ℕ) : (↑↑(a q t) + (↑(b q t)) • h7.β') ^ y ≠ 0 := fun H ↦ + h7.hirr (-(a q t : ℤ)) (b q t) <| by + have hEq : (a q t : ℂ) + b q t * h7.β = 0 := by + simpa [nsmul_eq_mul, map_add, map_mul, ← h7.habc.2.1] using + congrArg h7.σ (eq_zero_of_pow_eq_zero H) + push_cast + exact eq_div_iff_mul_eq (by unfold b; norm_cast) |>.mpr (by grind) + +include hq0 in +lemma b_sum_ne_zero : (↑q : h7.K) + q • h7.β' ≠ 0 := fun H ↦ + h7.hirr (-1) 1 <| by + have hEq : (q : ℂ) + q * h7.β = 0 := by + simpa [nsmul_eq_mul, ← h7.habc.2.1] using congrArg h7.σ H + have hqC : (q : ℂ) ≠ 0 := mod_cast Nat.ne_zero_of_lt hq0 + norm_num + exact mul_left_cancel₀ hqC (by linear_combination hEq) + +lemma bound_c₁β (q : ℕ) (hq0 : 0 < q) : 1 ≤ house ((h7.c₁ • (q + q • h7.β'))) := by + apply one_le_house_of_isIntegral (h7.isInt_β_bound q) + simp only [zsmul_eq_mul, ne_eq, mul_eq_zero, Int.cast_eq_zero, not_or] + refine ⟨Ne.symm (Int.ne_of_lt h7.one_le_c₁), h7.b_sum_ne_zero q hq0⟩ + +lemma one_le_house_c₁γ : 1 ≤ house (h7.c₁ • h7.γ') := by + apply one_le_house_of_isIntegral h7.isIntegral_c₁γ + simp only [zsmul_eq_mul, ne_eq, mul_eq_zero, Int.cast_eq_zero, not_or] + refine ⟨Ne.symm (Int.ne_of_lt h7.one_le_c₁), (h7.alpha'_beta'_gamma'_ne_zero).2.2⟩ + +/-- A large integer constant independent of `n` and `q`, used as a foundational base +to bound the houses (maximum absolute values of conjugates) of the algebraic coefficients. -/ +def c₂ : ℤ := (|h7.c₁| ^ (((1 + 2 * h7.m * (2 * h7.m))) + (1 + 2 * h7.m * (2 * h7.m)))) + +lemma one_le_c₂ : 1 ≤ h7.c₂ := by + apply le_trans (Int.cast_one_le_of_pos (h7.one_le_abs_c₁)) + nth_rw 1 [← pow_one (a:= |h7.c₁|)] + apply pow_le_pow_right₀ (h7.one_le_abs_c₁) (Nat.le_add_left 1 + ((1 + 2 * h7.m * (2 * h7.m)).add (Nat.add 1 (((2 * h7.m).mul + (Nat.mul 2 (2 * h7.h + 1) + 1)).add (Nat.mul 2 (2 * h7.h + 1) + 1))))) + +end Setup diff --git a/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAlgSetup.lean b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAlgSetup.lean new file mode 100644 index 00000000000000..a50811c7fef6c2 --- /dev/null +++ b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAlgSetup.lean @@ -0,0 +1,450 @@ +/- +Copyright (c) 2026 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ + +module + +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlg +public import Mathlib.Tactic + +/-! +# Gelfond-Schneider Theorem: Matrix Coefficient Bounds and Siegel's Lemma + +This file is the second component in the formalization of the Gelfond–Schneider Theorem + (Hilbert's Seventh Problem), establishing the transcendence of `α ^ β`. + +## Main results +Following the construction of the algebraic setup and linear system matrix in `MainAlg.lean`, +this file establishes strict analytical bounds on the coefficients of the matrix `A` and +applies Siegel's Lemma to guarantee a small, non-trivial integer solution. + +Specifically, we prove: +1. `house_matrixA_le`**: The maximum absolute value of the conjugates (the "house") of the + entries of `A` is strictly bounded by `c₃^n * n^((n - 1) / 2)`. +2. `η`**: The existence of a non-trivial vector of algebraic integers `η₁ ... η_t` in the kernel + of `A`. +3. `house_eta_le_c₄_pow`**: An explicit upper bound on the house of the solution vector `η`, + showing `‖ηₖ‖ ≤ c₄ⁿ * n^((n + 1) / 2)`. + +These bounded coefficients `η` will be used in subsequent files to explicitly construct the +auxiliary integer function `R(x)`. + +## References +* Loo-Keng Hua, Introduction to Number Theory, Springer, 1982. Chapter 17.9. +-/ + +@[expose] public section + +open BigOperators Module.Free Fintype NumberField Embeddings FiniteDimensional + Matrix Set Polynomial Finset IntermediateField Complex AnalyticAt + +noncomputable section + +variable (h7 : Setup) (q : ℕ) (hq0 : 0 < q) (u : Fin (h7.m * h7.n q)) (t : Fin (q * q)) + (h2mq : 2 * h7.m ∣ q ^ 2) + +namespace Setup + + +/-! +In this file we bound the house of the coefficients of the auxiliary function `R`; + `‖ηₖ‖ ≤ c₄ⁿ * n^((n - 1) / 2)`, for `1 ≤ k ≤ t`. +-/ + +open Real + +/-- A real-valued bounding constant encompassing `c₂` and the houses of `α'`, `β'`, and `γ'`. +Used to establish a strict upper bound on the entries of the linear system matrix `A`. -/ +def c₃ : ℝ := h7.c₂ * (1 + house h7.β') * sqrt (2 * h7.m) * + (max 1 (((house h7.α' ^ (2 * h7.m ^ 2)) * house h7.γ' ^(2 * h7.m ^ 2)))) + +lemma one_le_c₃ : 1 ≤ h7.c₃ := by + simp only [c₃] + refine one_le_mul_of_one_le_of_one_le ?_ (le_max_left 1 _) + refine one_le_mul_of_one_le_of_one_le ?_ ?_ + · exact one_le_mul_of_one_le_of_one_le (by exact_mod_cast h7.one_le_c₂) + (le_add_of_nonneg_right (house_nonneg _)) + · rw [one_le_sqrt] + have := h7.one_le_m + exact_mod_cast (by omega : 1 ≤ 2 * h7.m) + +lemma c₃_pow : h7.c₃ ^ ↑(h7.n q : ℝ) = h7.c₂ ^ ↑(h7.n q) * ((1 + house (h7.β')) ^ ↑(h7.n q)) * + (sqrt ((2 * h7.m)) ^ ↑(h7.n q)) * (max 1 ((house (h7.α') ^ (2 * h7.m ^ 2)) * house (h7.γ') ^ + (2*h7.m^ 2)))^ ↑(h7.n q) := by + simp only [c₃, rpow_natCast]; rw [mul_pow, mul_pow, mul_pow] + +include h2mq in +lemma q_sq_eq_two_mn : q ^ 2 = 2 * h7.m * h7.n q := Eq.symm (Nat.mul_div_cancel' h2mq) + +include h2mq in +lemma q_sq_le_two_mn : q ^ 2 ≤ 2 * h7.m * h7.n q := by + simpa using le_of_eq (h7.q_sq_eq_two_mn q h2mq) + +include h2mq in +lemma q_eq_n_etc : q ^ (h7.n q - 1) ≤ (sqrt (2 * h7.m) ^ (h7.n q - 1)) * (sqrt (h7.n q)) ^ + (h7.n q - 1) := by + rw [← mul_pow] + refine pow_le_pow_left₀ (by positivity) ?_ (h7.n q - 1) + have hq : (q : ℝ) ≤ sqrt (2 * h7.m * h7.n q) := by + refine (le_sqrt (by positivity) (by positivity)).2 (mod_cast h7.q_sq_le_two_mn q h2mq) + simpa [mul_assoc, sqrt_mul] using hq + +include h2mq in +lemma q_le_two_mn : q ≤ 2 * h7.m * h7.n q := + le_trans (Nat.le_pow (Nat.zero_lt_two)) ((by simpa using le_of_eq (h7.q_sq_eq_two_mn q h2mq))) + +include hq0 h2mq in +lemma m_mul_n_pos : 0 < h7.m * h7.n q := + Nat.mul_pos h7.one_le_m <| by simpa [n, Nat.div_pos_iff] using + ⟨Nat.zero_lt_succ (2 * h7.h + 1), Nat.le_of_dvd (Nat.pow_pos hq0) h2mq⟩ + +include h2mq hq0 in +lemma mul_div_sub_eq_one : ((h7.m : ℝ) * (h7.n q : ℝ) / (2 * (h7.m : ℝ) * (h7.n q : ℝ) - + (h7.m * (h7.n q : ℝ))) : ℝ) = 1 := by + have : 2 * (h7.m : ℝ) * (h7.n q : ℝ) - (h7.m : ℝ) * (h7.n q : ℝ) = (h7.m : ℝ) * (h7.n q : ℝ) := + by ring + rw [this] + exact div_self (by exact_mod_cast (h7.m_mul_n_pos q hq0 h2mq).ne') + +include hq0 h2mq in +lemma mul_rpow_sub_one_div_two : (h7.n q : ℝ) * (h7.n q : ℝ) ^ (((h7.n q : ℝ) - 1) / 2) = + (h7.n q : ℝ) ^ (((h7.n q : ℝ) + 1) / 2) := by + have h_exp : (((h7.n q : ℝ) + 1) / 2) = 1 + (((h7.n q : ℝ) - 1) / 2) := by ring + rw [h_exp, Real.rpow_add (by + norm_cast; refine Nat.ne_zero_iff_zero_lt.mp + (Nat.ne_zero_of_lt (one_le_n h7 q hq0 h2mq))), Real.rpow_one] + +include h2mq hq0 in +lemma abs_q_pow_mul_house_le_c₃_pow : |↑q| ^ (h7.n q - 1) * ((1 + house h7.β') ^ (h7.n q - 1) * + (house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * house h7.γ' ^ (h7.m * (2 * (h7.m * h7.n q))))) ≤ + (1 + house h7.β') ^ h7.n q * (√(2 * ↑h7.m) ^ h7.n q * (max 1 (house h7.α' ^ (2 * h7.m ^ 2) * + house h7.γ' ^ (2 * h7.m ^ 2)) ^ h7.n q * √↑(h7.n q) ^ (↑(h7.n q : ℝ) - 1))) := by + calc _ ≤ (sqrt (2 * h7.m) ^ (h7.n q -1))* (sqrt (h7.n q)) ^ ((h7.n q) -1) * + ((1 + house h7.β') ^ (h7.n q - 1) * (house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * + house h7.γ' ^ (h7.m * (2 * (h7.m * h7.n q))))) := ?_ + _ ≤ (sqrt (2 * h7.m) ^ (h7.n q -1)) * ((1 + house h7.β') ^ (h7.n q - 1) * + (house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * house h7.γ' ^ + (h7.m * (2 * (h7.m * h7.n q))))) * sqrt (h7.n q) ^ (((h7.n q) : ℝ) - 1) := ?_ + _ ≤ √(2 * ↑(h7.m)) ^ ((h7.n q)) * ((1 + house h7.β') ^ ((h7.n q)) * (house h7.α' ^ + (h7.m * 2 * h7.m)) ^ (h7.n q) * (house h7.γ' ^ (h7.m * 2 * h7.m)) ^ (h7.n q)) * + (sqrt (h7.n q )) ^ (((h7.n q) : ℝ)-1) := ?_ + · apply mul_le_mul (by simpa using (h7.q_eq_n_etc q h2mq)) (by rfl) (by dsimp [house];positivity) + (by positivity) + · have hsqrt : (sqrt (h7.n q) ^ (h7.n q - 1)) = (sqrt (h7.n q) ^ ((h7.n q : ℝ) - 1)) := by + simpa [(Nat.cast_sub (h7.one_le_n q hq0 h2mq))] using + (rpow_natCast (x := sqrt (h7.n q)) (n := h7.n q - 1)).symm + refine le_of_eq ?_; simp [hsqrt]; ac_rfl + · simp only [mul_assoc] + apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by positivity) + · refine Bound.pow_le_pow_right_of_le_one_or_one_le (Or.inl ⟨?_, by simp⟩) + have hm1 : (1 : ℝ) ≤ (h7.m : ℝ) := by exact_mod_cast h7.one_le_m + have : (1 : ℝ) ≤ (2 : ℝ) * (h7.m : ℝ) := by nlinarith + simpa [Nat.cast_mul, Nat.cast_ofNat] using (one_le_sqrt).2 this + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · refine Bound.pow_le_pow_right_of_le_one_or_one_le (Or.inl (by dsimp [house];simp)) + · apply mul_le_mul (by simp [pow_mul]) (by simp [pow_mul]) (by dsimp [house];positivity) + (pow_nonneg (pow_nonneg (house_nonneg _) _) _) + · nth_rw 2 [← mul_assoc] + rw [mul_comm ((1 + house h7.β') ^ (h7.n q)) (((sqrt ((2*h7.m)))) ^ (h7.n q))] + simp only [mul_assoc] + apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by positivity) + · refine pow_le_pow_left₀ (sqrt_nonneg _) (by rfl) (h7.n q) + · apply mul_le_mul (by rfl) ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · simp only [← mul_assoc] + apply mul_le_mul ?_ (by rfl) (by positivity) (by positivity) + · rw [← mul_pow] + refine pow_le_pow_left₀ (by dsimp [house];positivity) ?_ (h7.n q) + · have : ((h7.m * 2) * h7.m) = (2 * h7.m ^ 2) := by grind + rw [this]; clear this + calc _ ≤ house h7.α' ^ (2 * h7.m ^ 2) * house h7.γ' ^ (2 * h7.m ^ 2) := ?_ + _ ≤ max 1 ((house h7.α' ^ (2 * h7.m ^ 2) * house h7.γ' ^ (2 * h7.m ^ 2))) := ?_ + · apply Preorder.le_refl + · simp only [le_sup_right] + +lemma c₁_pow_sub_one_mul_c₁_pow_mul_c₁_pow_eq : + ((h7.c₁ : ℤ) ^ (h7.n q - 1) * (h7.c₁ : ℤ) ^ (h7.m * q) * (h7.c₁ : ℤ) ^ (h7.m * q)) = + ((h7.c₁ : ℤ) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁ : ℤ) ^ (h7.m * q - a q t * h7.l q u) * + (h7.c₁ : ℤ) ^ (h7.m * q - b q t * h7.l q u)) * ((h7.c₁ : ℤ) ^ h7.k q u * + (h7.c₁ : ℤ) ^ (a q t * h7.l q u) * (h7.c₁ : ℤ) ^ (b q t * h7.l q u)) := by + symm + calc _ = ((h7.c₁ : ℤ) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁ : ℤ) ^ h7.k q u) * + ((h7.c₁ : ℤ) ^ (h7.m * q - a q t * h7.l q u) * (h7.c₁ : ℤ) ^ (a q t * h7.l q u)) * + ((h7.c₁ : ℤ) ^ (h7.m * q - b q t * h7.l q u) * (h7.c₁ : ℤ) ^ (b q t * h7.l q u)) := ?_ + _ = _ := ?_ + · ring + · simp_rw [← pow_add] + have intCast_k_le_intCast_n_sub_one : (h7.k q u : ℤ) ≤ (h7.n q - 1 : ℤ) := by + have := (finProdFinEquiv.symm u).2.isLt + aesop + rw [Nat.sub_add_cancel (by grind), Nat.sub_add_cancel + (by simpa [mul_comm] using (Nat.mul_le_mul (((finProdFinEquiv.symm.toFun t).1).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt))), Nat.sub_add_cancel (by simpa [mul_comm] using + (Nat.mul_le_mul (((finProdFinEquiv.symm.toFun t).2).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt)))] + +lemma house_add_mul_le : + house (h7.c₁ • (↑(a q t) + b q t • h7.β')) ≤ (|h7.c₁| * |(q : ℤ)|) * (1 + house (h7.β')) := by + calc _ ≤ house (h7.c₁ • ((a q t : ℤ) : h7.K)) + house (h7.c₁ • ((b q t : ℤ) • h7.β')) := ?_ + _ ≤ house (h7.c₁ : h7.K) * house ((a q t : ℤ) : h7.K) + house (h7.c₁ : h7.K) * + house ((b q t : ℤ) • h7.β') := ?_ + _ ≤ house (h7.c₁ : h7.K) * house ((a q t : ℤ) : h7.K) + house (h7.c₁ : h7.K) * + (house ((b q t : ℤ) : h7.K) * house ( h7.β')) := ?_ + _ = |h7.c₁| * |(a q t : ℤ)| + |h7.c₁| * |(b q t : ℤ)| * house (h7.β') := ?_ + _ ≤ |h7.c₁| * |(q : ℤ)| + |h7.c₁| * |(q : ℤ)| * house h7.β' := ?_ + _ = |h7.c₁| * |(q : ℤ)| * (1 + house h7.β') := ?_ + · norm_cast; rw [smul_add]; apply house_add_le + · refine add_le_add (by grind [house_mul_le]) (by grind [house_mul_le]) + · refine add_le_add (by grind) + (mul_le_mul (le_refl _) (by grind [house_mul_le]) (house_nonneg _) (house_nonneg _)) + · rw [house_intCast]; rw [house_intCast]; rw [house_intCast]; rw [mul_assoc] + · refine add_le_add (mul_le_mul (le_refl _) (mod_cast ((finProdFinEquiv.symm.toFun t).1).isLt) + (Int.cast_nonneg (Int.zero_le_ofNat (a q t))) (Int.cast_nonneg (abs_nonneg (h7.c₁)))) ?_ + · rw [mul_assoc, mul_assoc] + apply mul_le_mul (by rfl) ?_ (mul_nonneg (by positivity) (house_nonneg _)) (by simp) + · apply mul_le_mul (mod_cast ((finProdFinEquiv.symm.toFun t).2).isLt) (le_refl _) + (house_nonneg _) (by simp) + · rw [mul_add]; simp only [Int.cast_abs, mul_one] + +/-! Moreover, the absolute value of the conjugates of the various coefficients is at most + `c₂^n (q + q * |β|) ^ (n - 1) * |α| ^ (m q) * |γ| ^ (m q) ≤ c₃^n * n^((n - 1) / 2)`. +-/ +include hq0 h2mq in +lemma house_matrixA_le : house ((algebraMap (𝓞 h7.K) h7.K) ((h7.A q) u t)) ≤ + (h7.c₃ ^ (h7.n q : ℝ) * (h7.n q : ℝ) ^ (((h7.n q : ℝ) - 1) / 2)) := by + simp only [A, systemCoeffs, RingOfIntegers.restrict, RingOfIntegers.map_mk] + calc _ = house (((h7.c₁ ^ (h7.n q - 1 - h7.k q u) * h7.c₁ ^ (h7.m * q - a q t * h7.l q u) * + h7.c₁ ^ (h7.m * q - b q t * h7.l q u)) • (h7.c₁ ^ h7.k q u * h7.c₁ ^ (a q t * h7.l q u) * + h7.c₁ ^ (b q t * h7.l q u))) • ((↑(a q t) + b q t • h7.β') ^ h7.k q u * h7.α' ^ + (a q t * h7.l q u) * h7.γ' ^ (b q t * h7.l q u))) := ?_ + _ = house ((h7.c₁ ^ ((h7.n q - 1) - h7.k q u) * h7.c₁ ^ (h7.m * q - a q t * h7.l q u) * + (h7.c₁ : h7.K) ^ (h7.m * q - b q t * h7.l q u)) • (((h7.c₁ : h7.K) ^ h7.k q u) * + ((a q t : h7.K) + (b q t) * h7.β') ^ h7.k q u * ((h7.c₁ : h7.K) ^ (a q t * h7.l q u)) * + h7.α' ^ (a q t * h7.l q u) * ((h7.c₁ : h7.K) ^ (b q t * h7.l q u)) * + h7.γ' ^ (b q t * h7.l q u))) := ?_ + _ ≤ house (((h7.c₁ : h7.K) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁ : h7.K) ^ + (h7.m * q - a q t * h7.l q u) * (h7.c₁ : h7.K) ^ (h7.m * q - b q t * h7.l q u))) * + house (h7.c₁ ^ (h7.k q u) • (↑(a q t) + (b q t) • h7.β') ^ (h7.k q u)) * + house (h7.c₁ ^ (a q t * h7.l q u) • h7.α' ^ (a q t * h7.l q u)) * + house (h7.c₁ ^ (b q t * h7.l q u) • h7.γ' ^ (b q t * h7.l q u)) := ?_ + _ ≤ house (((h7.c₁ : h7.K) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁ : h7.K) ^ + (h7.m * q - a q t * h7.l q u) * (h7.c₁ : h7.K) ^ (h7.m * q - b q t * h7.l q u))) * + house (h7.c₁ • (↑(a q t) + (b q t) • h7.β')) ^ (h7.k q u) * house (h7.c₁ • h7.α') ^ + (a q t * h7.l q u) * house (h7.c₁ • h7.γ') ^ (b q t * h7.l q u) := ?_ + _ ≤ house (((h7.c₁ : h7.K) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁ : h7.K) ^ + (h7.m * q - a q t * h7.l q u) * (h7.c₁ : h7.K) ^ (h7.m * q - b q t * h7.l q u))) * + house (h7.c₁ • (↑(a q t) + b q t • h7.β')) ^ (h7.n q - 1) * + house (h7.c₁ • h7.α') ^ (h7.m * q) * house (h7.c₁ • h7.γ') ^ (h7.m * q) := ?_ + _ ≤ |(((h7.c₁) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁) ^ (h7.m * q - a q t * h7.l q u) * + (h7.c₁) ^ (h7.m * q - b q t * h7.l q u)))| * (|h7.c₁| * + (|(q : ℤ)| * (1 + house (h7.β')))) ^ (h7.n q - 1) * (|h7.c₁| * house (h7.α')) ^ + (h7.m * (2 * (h7.m * h7.n q))) * (|h7.c₁| * house (h7.γ')) ^ + (h7.m * (2 * (h7.m * h7.n q))) := ?_ + _ = |(((h7.c₁) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁) ^ (h7.m * q - a q t * h7.l q u) * + (h7.c₁) ^ (h7.m * q - b q t * h7.l q u)))| * |h7.c₁ ^ (h7.n q - 1)| • + (↑|↑q| * (1 + house h7.β')) ^ (h7.n q - 1) * |h7.c₁ ^ (h7.m * (2 * (h7.m * h7.n q)))| • + house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * |h7.c₁ ^ (h7.m * (2 * (h7.m * h7.n q)))| + • house h7.γ' ^ (h7.m * (2 * (h7.m * h7.n q))) := ?_ + _ ≤ |(((h7.c₁) ^ (h7.n q - 1 - h7.k q u) * (h7.c₁) ^ (h7.m * q - a q t * h7.l q u) * + (h7.c₁) ^ (h7.m * q - b q t * h7.l q u)))| * ↑|h7.c₁| ^ ((h7.n q - 1) + + (2 * h7.m * (2 * (h7.m * h7.n q)))) * (↑|↑q| ^ ((h7.n q ) - 1) * (1 + house h7.β') ^ + (h7.n q - 1) * house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * + house h7.γ' ^ (h7.m * (2 * (h7.m * h7.n q)))) := ?_ + _ = |(h7.c₁) ^ (h7.n q - 1 - h7.k q u)| * |(h7.c₁) ^ (h7.m * q - a q t * h7.l q u)| * + |(h7.c₁) ^ (h7.m * q - b q t * h7.l q u)| * ↑|h7.c₁| ^ ((h7.n q - 1) + + (2 * h7.m * (2 * (h7.m * h7.n q)))) * (↑|↑q| ^ ((h7.n q)- 1) * (1 + house h7.β') + ^ (h7.n q - 1) * house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * house h7.γ' ^ + (h7.m * (2 * (h7.m * h7.n q)))) := ?_ + _ = |(h7.c₁)| ^ (h7.n q - 1 - h7.k q u) * |(h7.c₁)| ^ (h7.m * q - a q t * h7.l q u) * + |(h7.c₁)| ^ (h7.m * q - b q t * h7.l q u) * ↑|h7.c₁| ^ ((h7.n q - 1) + (2 * h7.m * + (2 * (h7.m * h7.n q)))) * (↑|↑q| ^ ((h7.n q) - 1) * (1 + house h7.β') ^ (h7.n q - 1) * + house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * + house h7.γ' ^ (h7.m * (2 * (h7.m * h7.n q)))) := ?_ + _ ≤ ↑(h7.c₂) ^ (h7.n q) * (↑|↑q| ^ ((h7.n q ) - 1) * (1 + house h7.β') ^ (h7.n q - 1) * + house h7.α' ^ (h7.m * (2 * (h7.m * h7.n q))) * + house h7.γ' ^ (h7.m * (2 * (h7.m * h7.n q)))) := ?_ + _ ≤ h7.c₃ ^ (h7.n q : ℝ) * ((sqrt (h7.n q)) ^ ((h7.n q : ℝ)- 1)) := ?_ + _ ≤ (h7.c₃ ^ (h7.n q : ℝ) * (h7.n q : ℝ) ^ (((h7.n q : ℝ) - 1) / 2)) := ?_ + · rw [c_coeffs] + conv => enter [2, 1]; simp only [Int.zsmul_eq_mul]; + rw [← c₁_pow_sub_one_mul_c₁_pow_mul_c₁_pow_eq] + · rw [smul_assoc]; simp; grind + · simp only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow,mul_assoc] + apply le_trans (house_mul_le _ _) (mul_le_mul (by rfl) ?_ (house_nonneg _) (house_nonneg _)) + · rw [← mul_assoc, ← mul_assoc, ← mul_assoc] + apply le_trans (house_mul_le _ _) + rw [← mul_assoc] + apply mul_le_mul (by grind [mul_assoc, house_mul_le]) (by rfl) (house_nonneg _) + (mul_nonneg (house_nonneg _) (house_nonneg _)) + · simp only [mul_assoc] + apply mul_le_mul (by rfl) ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · simp only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, ← mul_pow] + apply mul_le_mul (house_pow_le _ _) ?_ (by dsimp [house];positivity) + (by dsimp [house];positivity) + · apply mul_le_mul (house_pow_le _ _) (house_pow_le _ _) (house_nonneg _) + (pow_nonneg (house_nonneg _) _) + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · apply mul_le_mul (by rfl) ?_ (by dsimp [house];positivity) (house_nonneg _) + · refine Bound.pow_le_pow_right_of_le_one_or_one_le + (Or.inl ⟨one_le_house_of_isIntegral (isInt_β_bound_low _ _ _) (fun H ↦ ?_), ?_⟩) + · simp only [zsmul_eq_mul, mul_eq_zero, Int.cast_eq_zero] at H + cases H with + | inl hp => apply h7.c₁_ne_zero; exact hp + | inr hq => apply h7.β'_ne_zero q t 1; rw [pow_one]; exact hq + · refine (Nat.le_sub_iff_add_le' (h7.one_le_n q hq0 h2mq)).mpr ?_ + · rw [add_comm]; exact (finProdFinEquiv.symm.toFun u).2.isLt + · apply Bound.pow_le_pow_right_of_le_one_or_one_le + (Or.inl ⟨one_le_house_of_isIntegral h7.isIntegral_c₁α h7.c₁α_ne_zero, ?_⟩) + · rw [mul_comm h7.m q] + apply mul_le_mul (((finProdFinEquiv.symm.toFun t).1).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt) (zero_le _) (zero_le _) + · apply Bound.pow_le_pow_right_of_le_one_or_one_le + (Or.inl ⟨one_le_house_of_isIntegral h7.isIntegral_c₁γ h7.c₁γ_ne_zero, ?_⟩) + · rw [mul_comm h7.m q] + apply (mul_le_mul (((finProdFinEquiv.symm.toFun t).2).isLt) + (((finProdFinEquiv.symm.toFun u).1).isLt) (zero_le _) (zero_le _)) + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by dsimp [house];positivity) + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) + (by simp only [abs_mul, abs_pow, Int.cast_mul, Int.cast_pow, Int.cast_abs]; positivity) + · rw [← house_intCast (K := h7.K)]; simp + · refine pow_le_pow_left₀ (house_nonneg _) ?_ (h7.n q - 1) + · rw [← mul_assoc]; apply h7.house_add_mul_le q t + · calc _ ≤ house (h7.c₁ • h7.α') ^ (h7.m * (2 * (h7.m * h7.n q))) := ?_ + _ ≤ (↑|h7.c₁| * house h7.α') ^ (h7.m * (2 * (h7.m * h7.n q))) := ?_ + · refine Bound.pow_le_pow_right_of_le_one_or_one_le + (Or.inl ⟨one_le_house_of_isIntegral h7.isIntegral_c₁α h7.c₁α_ne_zero, ?_⟩) + · apply mul_le_mul (by rfl) ?_ (by simp) (by simp) + · exact (by have H := h7.q_le_two_mn q h2mq; rw [mul_assoc] at H; exact H ) + · refine pow_le_pow_left₀ (house_nonneg _) ?_ (h7.m * (2 * (h7.m * h7.n q))) + · calc _ ≤ house (h7.c₁ : h7.K) * house (h7.α') := ?_ + _ ≤ _ := ?_ + · grind [house_mul_le] + · simp + · calc _ ≤ house (h7.c₁ • h7.γ') ^ (h7.m * (2 * (h7.m * h7.n q))) := ?_ + _ ≤ (↑|h7.c₁| * house h7.γ') ^ (h7.m * (2 * (h7.m * h7.n q))) := ?_ + · refine Bound.pow_le_pow_right_of_le_one_or_one_le + (Or.inl ⟨one_le_house_of_isIntegral h7.isIntegral_c₁γ h7.c₁γ_ne_zero, ?_⟩) + · apply mul_le_mul (by rfl) (by grind [h7.q_le_two_mn q h2mq]) (by simp) (by simp) + refine pow_le_pow_left₀ (house_nonneg _) ?_ (h7.m * (2 * (h7.m * h7.n q))) + · calc _ ≤ house (h7.c₁ : h7.K) * house (h7.γ') := ?_ + _ ≤ _ := ?_ + · grind [house_mul_le] + · simp only [house_intCast, Int.cast_abs, le_refl] + · rw [zsmul_eq_mul, zsmul_eq_mul, zsmul_eq_mul, mul_pow, mul_pow, mul_pow, mul_pow, mul_pow, + abs_pow, abs_pow]; congr; all_goals simp + · have := zsmul_mul_mul_distrib |(h7.c₁ ^ (h7.n q - 1))| + |(h7.c₁ ^ (h7.m * (2 * (h7.m * h7.n q))))| + |(h7.c₁ ^ (h7.m * (2 * (h7.m * h7.n q))))| ((↑|↑q| * (1 + house (h7.β'))) ^ (h7.n q - 1)) + ((house h7.α') ^ (h7.m * (2 * (h7.m * h7.n q)))) + ((house h7.γ') ^ (h7.m * (2 * (h7.m * h7.n q)))) + simp only [mul_assoc, zsmul_eq_mul] at * + rw [← this, abs_pow, abs_pow, ← pow_add, ← pow_add] + apply mul_le_mul (by simp) ?_ (by dsimp [house];positivity) (by simp) + · apply mul_le_mul ?_ ?_ (by dsimp [house];positivity) (by simp) + · rw [← pow_add, ← pow_add, Eq.symm (Nat.two_mul (h7.m * (2 * (h7.m * h7.n q))))] + simp only [Int.cast_pow, Int.cast_abs, le_refl] + · rw [mul_pow]; simp only [mul_assoc]; simp only [Nat.abs_cast, le_refl] + · simp only [← pow_add, ← pow_add, Int.cast_abs, Int.cast_pow, Nat.abs_cast, abs_pow, + ← pow_add, ← pow_add, ← pow_add, ← pow_add] + · rw [abs_pow, abs_pow, abs_pow]; simp + · apply mul_le_mul ?_ (by rfl) (by dsimp [house];positivity) (?_) + · rw [← pow_add, ← pow_add, ← pow_add, Int.cast_abs, c₂, Int.cast_pow, Int.cast_abs, ← pow_mul] + refine pow_le_pow_right₀ (mod_cast h7.one_le_abs_c₁) ?_ + · simp only [add_mul, add_mul, one_mul, mul_assoc, + (Nat.two_mul (h7.m * (2 * (h7.m * h7.n q)))), add_assoc] + refine Nat.add_le_add ?_ (Nat.add_le_add ((Nat.sub_le _ _).trans <| by + simpa [mul_assoc] using Nat.mul_le_mul_left h7.m (h7.q_le_two_mn q h2mq)) + (Nat.add_le_add ((Nat.sub_le _ _).trans <| by + simpa [mul_assoc] using Nat.mul_le_mul_left h7.m (h7.q_le_two_mn q h2mq)) (by simp))) + · grind + · apply pow_nonneg; exact mod_cast (le_trans Int.one_nonneg (h7.one_le_c₂)) + · simp_rw [h7.c₃_pow q, mul_assoc] + apply mul_le_mul (by rfl) (h7.abs_q_pow_mul_house_le_c₃_pow q hq0 h2mq) + (by dsimp [house];positivity) ?_ + · apply pow_nonneg; norm_cast; apply le_trans Int.one_nonneg (h7.one_le_c₂) + · rw [le_iff_eq_or_lt]; left; + have : sqrt (h7.n q) ^ ((h7.n q : ℝ) - 1) = (h7.n q : ℝ) ^ (((h7.n q : ℝ) - 1) / 2) := by + nth_rw 1 [sqrt_eq_rpow, ← rpow_mul, mul_comm, mul_div] + · simp only [mul_one] + · simp only [Nat.cast_nonneg] + rw [← this] + +open NumberField + +include hq0 h2mq in +lemma hM_ne_zero : h7.A q ≠ 0 := by + intro H + let u : Fin _ := ⟨0, h7.m_mul_n_pos q hq0 h2mq⟩ + let t : Fin _ := ⟨0, mul_pos hq0 hq0⟩ + have H_eval : (h7.A q u t).val = 0 := by rw [H]; rfl + simp only [A, RingOfIntegers.restrict, zsmul_eq_mul, Int.cast_mul, Int.cast_pow] at H_eval + have hβ : (↑(a q t) + b q t • h7.β' : h7.K) ≠ 0 := fun h ↦ h7.β'_ne_zero q t 1 (by grind) + revert H_eval + simp [h7.c₁_ne_zero, h7.alpha'_beta'_gamma'_ne_zero.1, h7.alpha'_beta'_gamma'_ne_zero.2.2] + grind + +include hq0 h2mq in +lemma m_mul_n_lt_q_mul_q : h7.m * h7.n q < q * q := + lt_of_lt_of_eq (by grind [h7.m_mul_n_pos q hq0 h2mq]) <| + (h7.q_sq_eq_two_mn q h2mq).symm.trans (pow_two q) + +variable [DecidableEq (h7.K →+* ℂ)] + +/-- A non-trivial integer vector (in `𝓞 K`) residing in the kernel of the matrix `A`. +Its existence is guaranteed by Siegel's lemma (`exists_ne_zero_int_vec_house_le`). -/ +abbrev η : Fin (q * q) → 𝓞 h7.K := (house.exists_ne_zero_int_vec_house_le h7.K (h7.A q) + (h7.hM_ne_zero q hq0 h2mq) (mul_pos (Nat.zero_lt_succ (2 * h7.h + 1)) + (h7.one_le_n q hq0 h2mq)) (h7.m_mul_n_lt_q_mul_q q hq0 h2mq) (Fintype.card_fin _) + (fun u t ↦ h7.house_matrixA_le q hq0 u t h2mq) (Fintype.card_fin _)).choose + +/-- A real-valued bounding constant used to bound the norm (house) of the +solution vector `η`. -/ +def c₄ : ℝ := (max 1 ((house.c₁ h7.K) * house.c₁ h7.K * 2 * h7.m)) * h7.c₃ + +/-! +`‖ηₖ‖ ≤ c₄ⁿ * n^((n - 1) / 2)`, for `1 ≤ k ≤ t`. +-/ +open house in +include hq0 h2mq in +lemma house_eta_le_c₄_pow : house (algebraMap (𝓞 h7.K) h7.K (h7.η q hq0 h2mq t)) ≤ + h7.c₄ ^ (h7.n q : ℝ) * ((h7.n q : ℝ) ^ (((h7.n q : ℝ) + 1)/2)) := by + calc _ ≤ house.c₁ h7.K * (house.c₁ h7.K * ↑(q * q) * + (h7.c₃ ^ (h7.n q : ℝ) * (h7.n q : ℝ) ^ (((h7.n q : ℝ) - 1) / 2))) ^ + ((h7.m * h7.n q : ℝ) / (↑(q * q : ℝ) - ↑(h7.m * h7.n q ))) := ?_ + _ = (house.c₁ h7.K * (house.c₁ h7.K * 2 * h7.m * (h7.c₃ ^ (h7.n q : ℝ)) * ((h7.n q : ℝ) * + (h7.n q : ℝ) ^ (((h7.n q : ℝ) - 1) / 2)))) := ?_ + _ ≤ h7.c₄ ^ (h7.n q : ℝ) * ((h7.n q : ℝ) ^ (((h7.n q : ℝ) + 1) / 2) : ℝ) := ?_ + · exact mod_cast ((house.exists_ne_zero_int_vec_house_le + h7.K (h7.A q) (h7.hM_ne_zero q hq0 h2mq) (mul_pos (Nat.zero_lt_succ (2 * h7.h + 1)) + (h7.one_le_n q hq0 h2mq)) (h7.m_mul_n_lt_q_mul_q q hq0 h2mq) (Fintype.card_fin _) + (fun u t ↦ h7.house_matrixA_le q hq0 u t h2mq) (Fintype.card_fin _)).choose_spec).2.2 t + · have : (q * q : ℝ) = q^2 := mod_cast (pow_two ↑q).symm + rw [← pow_two q, this, h7.q_sq_eq_two_mn q h2mq] + have : (q ^ 2 : ℝ) = 2 * h7.m * h7.n q := mod_cast (h7.q_sq_eq_two_mn q h2mq) + rw [this] + have mul_div_sub_eq_one := h7.mul_div_sub_eq_one q hq0 h2mq + nth_rw 2 [← Nat.cast_mul] at mul_div_sub_eq_one + rw [mul_div_sub_eq_one, rpow_one, h7.mul_rpow_sub_one_div_two q hq0 h2mq, mul_eq_mul_left_iff] + left + rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc, mul_assoc] + have one_le_house_c₁ : 1 ≤ house.c₁ h7.K := one_le_mul_of_one_le_of_one_le (Nat.one_le_cast.mpr + (Module.finrank_pos)) (one_le_mul_of_one_le_of_one_le (le_max_left _ _) (le_max_left _ _)) + refine (mul_right_inj' (by grind)).mpr ?_ + · grind [h7.mul_rpow_sub_one_div_two q hq0 h2mq, ← mul_assoc, ← mul_assoc, ← mul_assoc] + · rw [h7.mul_rpow_sub_one_div_two q hq0 h2mq, ← mul_assoc, ← mul_assoc, ← mul_assoc, ← mul_assoc] + refine mul_le_mul_of_nonneg_right ?_ ?_ + · rw [c₄, mul_rpow (le_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _))) + (le_of_lt (lt_of_lt_of_le (by norm_num) h7.one_le_c₃))] + refine mul_le_mul_of_nonneg_right ?_ ?_ + · have hn : (1 : ℝ) ≤ (h7.n q : ℝ) := mod_cast h7.one_le_n q hq0 h2mq + have hpow : (max 1 (house.c₁ h7.K * house.c₁ h7.K * 2 * ↑h7.m) : ℝ) ≤ + (max 1 (house.c₁ h7.K * house.c₁ h7.K * 2 * ↑h7.m)) ^ (h7.n q : ℝ) := by + simpa [Real.rpow_one] using (rpow_le_rpow_of_exponent_le (le_max_left (1 : ℝ) _) hn) + exact (le_max_right (1 : ℝ) _).trans hpow + · apply rpow_nonneg (le_trans zero_le_one h7.one_le_c₃) + · apply rpow_nonneg; simp only [Nat.cast_nonneg] + +end Setup diff --git a/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAnalytic.lean b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAnalytic.lean new file mode 100644 index 00000000000000..53f250c209279f --- /dev/null +++ b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainAnalytic.lean @@ -0,0 +1,509 @@ +/- +Copyright (c) 2026 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ + +module + +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainOrder +public import Mathlib.Analysis.Analytic.Order + +/-! The goal of this file is to establish the critical lower bound for the proof of the +Gelfond-Schneider Theorem. Having constructed an auxiliary exponential polynomial +`R(x)` that vanishes to high order at specific points, we now isolate the first non-vanishing +derivative of `R(x)` and use its algebraic properties to bound it away from zero. + +## Main Objective + +To derive a contradiction, we need two opposing bounds on the size of the derivatives of `R(x)`. +This file is entirely dedicated to constructing the lower bound. +-/ + +@[expose] public section + +open BigOperators Module.Free Fintype NumberField Embeddings FiniteDimensional + Matrix Set Polynomial Finset IntermediateField Complex AnalyticAt + +noncomputable section + +variable (h7 : Setup) (q : ℕ) (hq0 : 0 < q) (u : Fin (h7.m * h7.n q)) + (t : Fin (q * q)) [DecidableEq (h7.K →+* ℂ)] (h2mq : 2 * h7.m ∣ q ^ 2) + +namespace Setup + +lemma iteratedkDeriv_R_eq_zero (k : Fin (h7.n q)) (l' : Fin (h7.m)) : + deriv^[k] (h7.R q hq0 h2mq) (l' + 1) = 0 := by + let u : Fin (h7.m * h7.n q) := (finProdFinEquiv.toFun ⟨l',k⟩) + have h1 := coeffs_mul_deriv_eq_zero h7 q hq0 u h2mq + unfold Setup.k at * + unfold Setup.l at * + unfold u at * + simp only [Equiv.toFun_as_coe, + Equiv.symm_apply_apply] at * + have : (h7.σ (h7.c_coeffs q) * + (Complex.log h7.α)^(-k : ℤ)) * deriv^[k] (h7.R q hq0 h2mq) (l'+1) = + (h7.σ (h7.c_coeffs q) * + (Complex.log h7.α)^(-k : ℤ)) * 0 → deriv^[k] (h7.R q hq0 h2mq) (l' + 1) = 0 := by + apply mul_left_cancel₀ + by_contra H + simp only [Int.cast_mul, Int.cast_pow, map_mul, map_pow, + map_intCast, zpow_neg, zpow_natCast, + mul_eq_zero, pow_eq_zero_iff', Int.cast_eq_zero, ne_eq, not_or, inv_eq_zero] at H + rcases H with ⟨h1, h2⟩ + · apply h7.c₁_ne_zero; assumption + · apply h7.c₁_ne_zero; rename_i h2; exact h2.1 + · apply h7.c₁_ne_zero; rename_i h2; exact h2.1 + · have : Complex.log h7.α ≠ 0 := + mt (fun h ↦ by simpa [exp_log h7.htriv.1, exp_zero] using congrArg exp h) h7.htriv.2 + apply this; rename_i h2; exact h2.1 + rw [this] + rw [mul_zero] + rw [mul_assoc] + simp only [mul_assoc] at * + rw [← h1] + simp only [Int.cast_mul, Int.cast_pow, map_mul, map_pow, map_intCast, zpow_neg, zpow_natCast, + Nat.cast_add, Nat.cast_one] + +open AnalyticOnNhd + +lemma order_neq_top : ∀ (l' : Fin (h7.m)), analyticOrderAt (h7.R q hq0 h2mq) (l' + 1) ≠ ⊤ := by + intros l' H + rw [analyticOrderAt_eq_top_iff_eq_zero] at H + · apply h7.R_ne_zero q hq0 h2mq (by aesop) + fun_prop + +lemma order_neq_top_min_one : ∀ z : ℂ, analyticOrderAt (h7.R q hq0 h2mq) z ≠ ⊤ := by + intros l' H + rw [analyticOrderAt_eq_top_iff_eq_zero] at H + · apply h7.R_ne_zero + · rw [funext_iff] + intros z + rw [funext_iff] at H + apply H z + intros z + fun_prop + +lemma Rorder_exists (z : ℂ) : + ∃ r, (analyticOrderAt (h7.R q hq0 h2mq) z) = some r := by + have : (analyticOrderAt (h7.R q hq0 h2mq) z) ≠ ⊤ := + h7.order_neq_top_min_one q hq0 h2mq z + revert this + cases (analyticOrderAt (h7.R q hq0 h2mq) z) with + | top => grind + | coe => aesop + +def R_order (z : ℂ) : ℕ := (Rorder_exists h7 q hq0 h2mq z).choose + +def R_order_prop {z : ℂ} := (Rorder_exists h7 q hq0 h2mq z).choose_spec + +lemma R_order_eq (z) : (analyticOrderAt (h7.R q hq0 h2mq) z) = h7.R_order q hq0 h2mq z := + (Rorder_exists h7 q hq0 h2mq z).choose_spec + +lemma r_exists : ∃ r, r' h7 q hq0 h2mq = some r := by + have H := order_neq_top_min_one h7 q hq0 h2mq (l₀' h7 q hq0 h2mq + 1) + have : r' h7 q hq0 h2mq ≠ ⊤ := by rw [(r'_spec h7 q hq0 h2mq).1] at H; exact H + revert this + cases r' h7 q hq0 h2mq with + | top => grind + | coe => aesop + +def r := (r_exists h7 q hq0 h2mq).choose + +abbrev r_spec : h7.r' q hq0 h2mq = ↑(h7.r q hq0 h2mq) := + (r_exists h7 q hq0 h2mq).choose_spec + +abbrev r_prop : + let s : Finset (Fin (h7.m)) := Finset.univ + analyticOrderAt (h7.R q hq0 h2mq) (h7.l₀' q hq0 h2mq + 1) = h7.r q hq0 h2mq ∧ + ∀ l' ∈ s, h7.r q hq0 h2mq ≤ analyticOrderAt (h7.R q hq0 h2mq) (↑↑l' + 1) := by + intros s + rw [← h7.r_spec q hq0 h2mq] + apply h7.r'_spec q hq0 h2mq + +lemma r_div_q_geq_0 : 0 ≤ (h7.r q hq0 h2mq) / q := by simp_all only [zero_le] + + +def cρ : ℤ := abs (h7.c₁ ^ (h7.r q hq0 h2mq) * h7.c₁^(2*h7.m * q)) + +abbrev systemCoeffs_r : h7.K := (a q t + b q t • h7.β')^(h7.r q hq0 h2mq) * + h7.α' ^(a q t * (h7.l₀' q hq0 h2mq + 1)) * h7.γ' ^(b q t * (h7.l₀' q hq0 h2mq + 1)) + +lemma systemCoeffs_ne_zero_r : h7.systemCoeffs_r q hq0 t h2mq ≠ 0 := by + unfold systemCoeffs_r + intros H + simp only [mul_eq_zero, pow_eq_zero_iff'] at H + cases H with + | inl H1 => + cases H1 with + | inl H1 => + rcases H1 with ⟨h1, h2⟩ + apply (h7.β'_ne_zero q t (h7.r q hq0 h2mq)) + rw [h1] + simp only [pow_eq_zero_iff', ne_eq, true_and] + exact h2 + | inr H2 => exact h7.alpha'_beta'_gamma'_ne_zero.1 H2.1 + | inr H2 => + exfalso + exact h7.alpha'_beta'_gamma'_ne_zero.2.2 H2.1 + +def ρᵣ : ℂ := (Complex.log h7.α)^(-(h7.r q hq0 h2mq) : ℤ) * + deriv^[h7.r q hq0 h2mq] (h7.R q hq0 h2mq) (h7.l₀' q hq0 h2mq + 1) + +lemma systemCoeffs_map_eq_exp_mul_r : + exp (h7.ρ q t * (h7.l₀' q hq0 h2mq + 1)) * + h7.ρ q t ^ (h7.r q hq0 h2mq : ℕ) * + Complex.log h7.α ^ (-(h7.r q hq0 h2mq) : ℤ) = h7.σ (h7.systemCoeffs_r q hq0 t h2mq) := by + nth_rw 2 [ρ] + rw [mul_pow, mul_assoc, mul_assoc] + have : (Complex.log h7.α ^ (h7.r q hq0 h2mq : ℕ) * + Complex.log h7.α ^ (-h7.r q hq0 h2mq : ℤ)) = 1 := by + simp only [zpow_neg, zpow_natCast] + refine Complex.mul_inv_cancel ?_ + by_contra! H + have : Complex.log h7.α ≠ 0 := + mt (fun h ↦ by simpa [exp_log h7.htriv.1, exp_zero] using congrArg exp h) h7.htriv.2 + apply this + simp only [pow_eq_zero_iff', ne_eq] at H + apply H.1 + rw [this]; clear this + rw [mul_one] + unfold systemCoeffs_r + rw [mul_comm] + change _ = h7.σ ((↑(a q t) + b q t • h7.β') ^ (h7.r q hq0 h2mq : ℕ) + * (h7.α' ^ (a q t * (h7.l₀' q hq0 h2mq + 1))) * (h7.γ' ^ (b q t * (h7.l₀' q hq0 h2mq + 1)))) + rw [map_mul] + rw [map_mul] + nth_rw 1 [mul_assoc] + have : h7.σ ((↑(a q t) + (b q t) • h7.β') ^ (h7.r q hq0 h2mq)) = + (↑(a q t) + ↑(b q t) * h7.β) ^ ((h7.r q hq0 h2mq)) := by + simp only [nsmul_eq_mul, map_pow, map_add, map_natCast, map_mul] + simp_all only [a, b] + congr + rw [h7.habc.2.1] + rw [this]; clear this + rw [map_pow, map_pow] + have : (↑(a q t) + (b q t) • h7.β) ^ + (h7.r q hq0 h2mq) * cexp (h7.ρ q t * (h7.l₀' q hq0 h2mq + 1)) = + (↑(a q t) + ↑(b q t) * h7.β)^(h7.r q hq0 h2mq) * + cexp (h7.ρ q t * (h7.l₀' q hq0 h2mq + 1)) := by + simp_all only [Equiv.toFun_as_coe, finProdFinEquiv_symm_apply, + Fin.coe_modNat, + Fin.coe_divNat, Nat.cast_add, Nat.cast_one, nsmul_eq_mul,b, a] + rw [this]; clear this + simp only [mul_eq_mul_left_iff, pow_eq_zero_iff'] + left + rw [ρ] + have : cexp (( ↑(a q t) + (b q t) • h7.β) * Complex.log h7.α * (h7.l₀' q hq0 h2mq + 1) + ) = + cexp ((↑(a q t) + ↑(b q t) • h7.β) * Complex.log h7.α * (h7.l₀' q hq0 h2mq +1)) := by + simp_all only [Equiv.toFun_as_coe, finProdFinEquiv_symm_apply, + Fin.coe_modNat, + Fin.coe_divNat, Nat.cast_add, Nat.cast_one, + nsmul_eq_mul, b, a] + rw [this];clear this + have : h7.σ h7.α' ^ ((a q t) * (h7.l₀' q hq0 h2mq + 1)) * + h7.σ h7.γ' ^ ((b q t) * (h7.l₀' q hq0 h2mq + 1)) = + h7.α ^ ((a q t) * (h7.l₀' q hq0 h2mq + 1)) * + (h7.σ h7.γ')^ ((b q t) * (h7.l₀' q hq0 h2mq + 1)) := by + simp only [mul_eq_mul_right_iff, pow_eq_zero_iff', + map_eq_zero, ne_eq, mul_eq_zero, not_or] + left + congr + rw [← h7.habc.1] + rw [← h7.habc.1] + have : h7.σ h7.γ' = h7.α^h7.β := by rw [h7.habc.2.2] + rw [this]; clear this + have : Complex.exp (Complex.log h7.α) = h7.α := + Complex.exp_log h7.htriv.1 + clear this + rw [← cpow_nat_mul] + have : cexp ((↑(a q t) + (b q t) • h7.β) * + Complex.log h7.α * (h7.l₀' q hq0 h2mq +1)) = + h7.α ^ ((a q t) * (h7.l₀' q hq0 h2mq + 1)) * + h7.α ^ (↑((b q t) * (h7.l₀' q hq0 h2mq +1 )) * h7.β) ↔ + cexp ((↑(a q t) + (b q t) • h7.β) * + Complex.log h7.α * (h7.l₀' q hq0 h2mq + 1)) = + h7.α ^ (((a q t) * (h7.l₀' q hq0 h2mq +1)) + + ((↑(b q t) * (h7.l₀' q hq0 h2mq + 1)) * h7.β)) := by + rw [cpow_add] + · simp only [nsmul_eq_mul, Nat.cast_mul] + norm_cast + exact h7.htriv.1 + rw [this]; clear this + rw [cpow_def_of_ne_zero] + · have : Complex.log h7.α * (↑(a q t) * (h7.l₀' q hq0 h2mq +1) + + ((b q t) * (h7.l₀' q hq0 h2mq + 1)) * h7.β) = + (↑(a q t) + (b q t) • h7.β) * Complex.log h7.α * (h7.l₀' q hq0 h2mq + 1) := by + nth_rw 4 [mul_comm] + have : ( ((h7.l₀' q hq0 h2mq + 1) * (b q t)) * h7.β) = + ( (((b q t) * h7.β) * (h7.l₀' q hq0 h2mq + 1))) := by + exact mul_rotate (↑↑(h7.l₀' q hq0 h2mq) + 1) (↑(b q t)) h7.β + rw [this];clear this + have H : (↑(a q t) * (h7.l₀' q hq0 h2mq + 1) + + (((b q t) * h7.β) * (h7.l₀' q hq0 h2mq +1))) = + (((a q t) + ((b q t) * h7.β)) * ↑((↑(h7.l₀' q hq0 h2mq : ℕ) + 1 :ℂ))) := + Eq.symm (RightDistribClass.right_distrib + (↑(a q t)) (↑(b q t) * h7.β) (h7.l₀' q hq0 h2mq + 1)) + rw [H, mul_comm, mul_assoc] + nth_rw 3 [mul_comm] + rw [← mul_assoc, nsmul_eq_mul] + rw [this] + · exact h7.htriv.1 + +def deriv_R_k_eval_at_l0' : + deriv^[h7.r q hq0 h2mq] (h7.R q hq0 h2mq) (h7.l₀' q hq0 h2mq + 1) = + ∑ t, h7.σ ((h7.η q hq0 h2mq) t) * + cexp (h7.ρ q t * (h7.l₀' q hq0 h2mq + 1)) * (h7.ρ q t) ^ (h7.r q hq0 h2mq) := by + rw [iteratedDeriv_R] + +lemma systemCoeffs_deriv_r : + (Complex.log h7.α)^(-h7.r q hq0 h2mq : ℤ) * deriv^[h7.r q hq0 h2mq] + (h7.R q hq0 h2mq) (h7.l₀' q hq0 h2mq + 1) = + ∑ t, h7.σ ↑((h7.η q hq0 h2mq) t) * h7.σ (h7.systemCoeffs_r q hq0 t h2mq) := by + rw [h7.deriv_R_k_eval_at_l0' q hq0 h2mq, mul_sum, Finset.sum_congr rfl] + intros t ht + rw [mul_assoc, mul_comm, mul_assoc] + unfold η + simp only [mul_eq_mul_left_iff, map_eq_zero, + FaithfulSMul.algebraMap_eq_zero_iff] + left + have := systemCoeffs_map_eq_exp_mul_r h7 q hq0 t h2mq + rw [← this] + +def rho := ∑ t : Fin (q * q), (h7.η q hq0 h2mq t) * (h7.systemCoeffs_r q hq0 t h2mq) + +def rho_eq_ρᵣ : h7.σ (rho h7 q hq0 h2mq) = ρᵣ h7 q hq0 h2mq := by + unfold rho ρᵣ + rw [systemCoeffs_deriv_r] + simp only [map_sum, map_mul, nsmul_eq_mul, map_pow, map_add, map_natCast] + +lemma cρ_ne_zero : h7.cρ q hq0 h2mq ≠ 0 := by + apply abs_ne_zero.mpr <| mul_ne_zero _ _ + all_goals apply pow_ne_zero _ (h7.c₁_ne_zero) + +/-! +This number lies in $K,$ and ${c_1}^{r+2mq}\rho$ is an integer in $K$ +-/ + +lemma ρ_is_int : + IsIntegral ℤ (h7.cρ q hq0 h2mq • rho h7 q hq0 h2mq) := by + unfold rho cρ systemCoeffs_r + have : h7.c₁ ^ (2 * h7.m * q) = h7.c₁ ^ (h7.m * q) + * h7.c₁ ^ (h7.m * q) := by + rw [← pow_add]; ring + rw [this] + rcases abs_choice (h7.c₁ ^ h7.r q hq0 h2mq * h7.c₁ ^ (h7.m * q) * h7.c₁ ^ (h7.m * q)) with H1 | H2 + · rw [← mul_assoc, H1, Finset.smul_sum] + apply IsIntegral.sum + intros x hx + rw [zsmul_eq_mul] + nth_rw 1 [mul_comm] + rw [mul_assoc] + apply IsIntegral.mul + · exact RingOfIntegers.isIntegral_coe ((h7.η q hq0 h2mq) x) + · rw [mul_comm, ← zsmul_eq_mul] + have triple_comm (K : Type) [Field K] (a b c : ℤ) (x y z : K) : + ((a*b)*c) • ((x*y)*z) = a•x * b•y * c•z := by + simp only [zsmul_eq_mul, Int.cast_mul]; ring + have := triple_comm h7.K + (h7.c₁^(h7.r q hq0 h2mq) : ℤ) + (h7.c₁^(h7.m * q) : ℤ) + (h7.c₁^(h7.m * q) : ℤ) + (((a q x : ℕ) + b q x • h7.β')^(h7.r q hq0 h2mq)) + (h7.α' ^ (a q x * (h7.l₀' q hq0 h2mq + 1))) + (h7.γ' ^ (b q x * (h7.l₀' q hq0 h2mq + 1))) + have : IsIntegral ℤ + ((h7.c₁ ^ (h7.r q hq0 h2mq) * h7.c₁ ^ (h7.m * q) * h7.c₁ ^ (h7.m * q)) • + ((↑(a q x) + b q x • h7.β') ^ (h7.r q hq0 h2mq) * + h7.α' ^ (a q x * (h7.l₀' q hq0 h2mq + 1)) * + h7.γ' ^ (b q x * (h7.l₀' q hq0 h2mq + 1)))) = + IsIntegral ℤ + (h7.c₁ ^ (h7.r q hq0 h2mq) • (↑(a q x) + b q x • h7.β') ^ (h7.r q hq0 h2mq) * + h7.c₁ ^ (h7.m * q) • h7.α' ^ (a q x * (h7.l₀' q hq0 h2mq + 1)) * + h7.c₁ ^ (h7.m * q) • h7.γ' ^ (b q x * (h7.l₀' q hq0 h2mq + 1))) := by + rw [← this] + simp_rw [this] + apply IsIntegral.mul + · apply IsIntegral.mul + · simp only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow] + rw [← mul_pow] + apply IsIntegral.pow + rw [mul_add] + apply IsIntegral.add + · apply IsIntegral.mul <| IsIntegral.Cast _ _ + · apply IsIntegral.Nat + · rw [mul_comm, mul_assoc] + apply IsIntegral.mul + · apply IsIntegral.Nat + · rw [mul_comm]; + have := h7.isIntegral_c₁β + simp only [zsmul_eq_mul] at this + exact this + · apply h7.isIntegral_c₁_pow_smul_pow + · rw [mul_comm] + apply Nat.mul_le_mul ((h7.l₀' q hq0 h2mq).isLt) ((finProdFinEquiv.symm.toFun x).1.isLt) + · rw [← zsmul_eq_mul]; exact h7.isIntegral_c₁α + · have : h7.c₁ ^ (h7.m * q - ((b q x) * (h7.l₀' q hq0 h2mq + 1))) * + (h7.c₁ ^ ((b q x) * (h7.l₀' q hq0 h2mq + 1))) = + (h7.c₁ ^ ((h7.m * q))) := by + rw [← pow_add,Nat.sub_add_cancel] + nth_rw 1 [mul_comm] + apply mul_le_mul + · exact (h7.l₀' q hq0 h2mq).isLt + · exact (finProdFinEquiv.symm.toFun x).2.isLt + · simp only [zero_le] + · simp only [zero_le] + rw [← this] + simp only [zsmul_eq_mul, Int.cast_mul, Int.cast_pow] + rw [mul_assoc] + apply IsIntegral.mul + · apply IsIntegral.pow + · apply IsIntegral.Cast + · rw [← mul_pow] + apply IsIntegral.pow + · rw [← zsmul_eq_mul]; exact h7.isIntegral_c₁γ + · rw [Finset.smul_sum] + apply IsIntegral.sum + intros x hx + rw [← mul_assoc, H2] + rw [zsmul_eq_mul] + nth_rw 1 [mul_comm] + rw [mul_assoc] + apply IsIntegral.mul + · exact RingOfIntegers.isIntegral_coe ((h7.η q hq0 h2mq) x) + · rw [mul_comm] + rw [← zsmul_eq_mul] + have triple_comm (K : Type) [Field K] (a b c : ℤ) (x y z : K) : + ((a*b)*c) • ((x*y)*z) = a•x * b•y * c•z := by + simp only [zsmul_eq_mul, Int.cast_mul]; ring + have H := triple_comm h7.K + (h7.c₁^(h7.r q hq0 h2mq)) + (h7.c₁^(h7.m * q) : ℤ) + (h7.c₁^(h7.m * q) : ℤ) + (((a q x : ℕ) + (b q x) • h7.β')^(h7.r q hq0 h2mq)) + (h7.α' ^ ((a q x) * ((h7.l₀' q hq0 h2mq + 1)))) + (h7.γ' ^ ((b q x) * ((h7.l₀' q hq0 h2mq + 1)))) + have : IsIntegral ℤ (-(h7.c₁ ^ h7.r q hq0 h2mq * h7.c₁ ^ (h7.m * q) * h7.c₁ ^ (h7.m * q)) • + ((↑(a q x) + b q x • h7.β') ^ h7.r q hq0 h2mq * h7.α' ^ (a q x * (h7.l₀' q hq0 h2mq + 1)) * + h7.γ' ^ (b q x * (h7.l₀' q hq0 h2mq + 1)))) = + IsIntegral ℤ ((h7.c₁ ^ (h7.r q hq0 h2mq) • + (↑(a q x) + (b q x) • h7.β') ^ (h7.r q hq0 h2mq) + * h7.c₁ ^ (h7.m * q) • h7.α' ^ ((a q x) * + (h7.l₀' q hq0 h2mq + 1)) * h7.c₁ ^ (h7.m * q) • + h7.γ' ^ ((b q x) * (h7.l₀' q hq0 h2mq + 1)))) := by + rw [← H] + rw [neg_smul] + simp only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_mul, Int.cast_pow, + IsIntegral.neg_iff] + clear H + rw [this] + apply IsIntegral.mul + · apply IsIntegral.mul + · simp only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow] + rw [← mul_pow] + apply IsIntegral.pow + rw [mul_add] + · apply IsIntegral.add + · apply IsIntegral.mul <| IsIntegral.Cast _ _ + · apply IsIntegral.Nat + ·rw [mul_comm, mul_assoc] + apply IsIntegral.mul <| IsIntegral.Nat _ _ + rw [mul_comm, ← zsmul_eq_mul] + exact h7.isIntegral_c₁β + · apply h7.isIntegral_c₁_pow_smul_pow + · rw [mul_comm] + apply Nat.mul_le_mul + · exact (h7.l₀' q hq0 h2mq).isLt + exact (finProdFinEquiv.symm.toFun x).1.isLt + · rw [← zsmul_eq_mul]; exact h7.isIntegral_c₁α + · have : h7.c₁ ^ (h7.m * q - (b q x * (h7.l₀' q hq0 h2mq + 1))) * + (h7.c₁ ^ ((b q x) * (h7.l₀' q hq0 h2mq + 1))) = (h7.c₁ ^ ((h7.m * q))) := by + rw [← pow_add, Nat.sub_add_cancel] + nth_rw 1 [mul_comm] + apply mul_le_mul + · exact (h7.l₀' q hq0 h2mq).isLt + · exact (finProdFinEquiv.symm.toFun x).2.isLt + · simp only [zero_le] + · simp only [zero_le] + rw [← this] + simp only [zsmul_eq_mul, Int.cast_mul, Int.cast_pow] + rw [mul_assoc] + apply IsIntegral.mul + · apply IsIntegral.pow + · apply IsIntegral.Cast + · rw [← mul_pow] + apply IsIntegral.pow + · rw [← zsmul_eq_mul]; exact h7.isIntegral_c₁γ + +def c1ρ : 𝓞 h7.K := RingOfIntegers.restrict _ + (fun _ => (ρ_is_int h7 q hq0 h2mq)) ℤ + +lemma one_le_c1rho : 1 ≤ ↑(h7.cρ q hq0 h2mq) := by + apply Int.one_le_abs + by_contra H + simp only [mul_eq_zero, pow_eq_zero_iff', ne_eq, + OfNat.ofNat_ne_zero, false_or, not_or] at H + cases H with + | inl h1 => apply (h7.c₁_ne_zero); exact h1.1 + | inr h2 => apply (h7.c₁_ne_zero); exact h2.1 + +lemma one_le_norm_c1rho : 1 ≤ norm (h7.cρ q hq0 h2mq) := by + have := one_le_c1rho h7 q hq0 h2mq + have : |(h7.cρ q hq0 h2mq)| = ‖(h7.cρ q hq0 h2mq : ℤ)‖ := by + simp only [Int.cast_abs] + exact rfl + rw [← this] + simp only [Int.cast_abs, ge_iff_le] + have := Int.one_le_abs (z := h7.cρ q hq0 h2mq) + norm_cast + apply this + exact cρ_ne_zero h7 q hq0 h2mq + +lemma zero_le_c1rho : 0 ≤ ↑(h7.cρ q hq0 h2mq) := + Int.le_of_lt (one_le_c1rho h7 q hq0 h2mq) + +lemma crho_le_abs_crho : + (h7.cρ q hq0 h2mq) ≤ abs (h7.cρ q hq0 h2mq):= le_abs_self _ + +lemma abs_crho_le_norm_crho : + abs (h7.cρ q hq0 h2mq) ≤ norm (h7.cρ q hq0 h2mq) := by + simp only [Int.cast_abs] + rfl + +lemma norm_crho_le_house_crho : norm (h7.cρ q hq0 h2mq) ≤ + house (h7.cρ q hq0 h2mq : h7.K) := by + rw [house_intCast] + simp only [Int.cast_abs] + exact Preorder.le_refl ‖h7.cρ q hq0 h2mq‖ + +lemma norm_cρ_pos : 0 < ‖h7.cρ q hq0 h2mq‖ := by + rw [norm_pos_iff] + have := h7.cρ_ne_zero q hq0 h2mq + unfold cρ at this + exact this + +lemma h1 : 1 ≤ ‖h7.cρ q hq0 h2mq‖ ^ Module.finrank ℚ h7.K := by + rw [one_le_pow_iff_of_nonneg] + · rw [Int.norm_eq_abs] + have := (h7.norm_cρ_pos q hq0 h2mq) + rw [Int.norm_eq_abs] at this + unfold cρ + simp only [Int.cast_abs, Int.cast_mul, Int.cast_pow, abs_abs] + rw [← pow_add] + simp only [abs_pow] + have : 1 ≤ |↑(h7.c₁)| := by + rw [le_abs'] + right + exact h7.one_le_c₁ + refine one_le_pow₀ ?_ + exact mod_cast this + · apply norm_nonneg + · have : 0 < Module.finrank ℚ h7.K := Module.finrank_pos + simp_all only [ne_eq] + intro a + simp_all only [lt_self_iff_false] + +end Setup + +end diff --git a/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainOrder.lean b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainOrder.lean new file mode 100644 index 00000000000000..a29dc7aa0fa0f2 --- /dev/null +++ b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainOrder.lean @@ -0,0 +1,272 @@ +/- +Copyright (c) 2026 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ + +module + +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlgSetup +public import Mathlib.Analysis.Analytic.Order + +/-! +This PR is the third component in the formalization of the Gelfond-Schneider Theorem +(Hilbert's Seventh Problem). It connects the algebraically constructed auxiliary function `R(x)` +to its analytical properties, establishing the exact order of vanishing and the fundamental lower +bound on the norm of its non-zero derivative evaluation. + +Following the argument in Loo-Keng Hua's "Introduction to Number Theory" +Chapter 17.9, equations (4) and (5)), we define the minimal non-vanishing derivative +order $r$ and scale the evaluation to an algebraic integer to compute its norm. +-/ + +@[expose] public section + +open BigOperators Module.Free Fintype NumberField Embeddings FiniteDimensional + Matrix Set Polynomial Finset IntermediateField Complex AnalyticAt + +noncomputable section + +variable (h7 : Setup) (q : ℕ) (hq0 : 0 < q) (u : Fin (h7.m * h7.n q)) + (t : Fin (q * q)) [DecidableEq (h7.K →+* ℂ)] (h2mq : 2 * h7.m ∣ q ^ 2) + +/-! +Since the numbers `ρ₁, ..., ρₜ` are distinct, the function `R(x)` +is not identically zero. For suppose otherwise, then on expanding the right +hand side of `R` we have `η₁ρ₁ + η₂ρ₂ᵏ + ... + ηₜρₜᵏ = 0`, a contradiction. +-/ + +lemma eq_iff_finProdFinEquiv_symm_ext (i j : Fin (q * q)) : i = j ↔ + (finProdFinEquiv.symm.1 i).1 = (finProdFinEquiv.symm.1 j).1 ∧ + ((finProdFinEquiv.symm.1 i).2 : Fin q) = (finProdFinEquiv.symm.1 j).2 := by + rw [← Prod.ext_iff, Equiv.toFun_as_coe, EmbeddingLike.apply_eq_iff_eq] + +namespace Setup + +omit [DecidableEq (h7.K →+* ℂ)] in +lemma rho_injective (i j : Fin (q * q)) (hij : i ≠ j) : ρ h7 q i ≠ ρ h7 q j := by + rw [ne_eq, eq_iff_finProdFinEquiv_symm_ext q, not_and'] at hij + simp only [ρ, not_or, ne_eq, mul_eq_mul_right_iff, not_or] + constructor + · by_cases Heq : (finProdFinEquiv.symm.1 i).2 = (finProdFinEquiv.symm.1 j).2 + · unfold a b + rw [Heq] + intro H + apply (hij Heq) + simp only [Equiv.toFun_as_coe, nsmul_eq_mul, add_left_inj, Nat.cast_inj] at H + exact Fin.eq_of_val_eq H + · let i2 : ℕ := (finProdFinEquiv.symm.toFun i).2 + 1 + let j2 : ℕ := (finProdFinEquiv.symm.toFun j).2 + 1 + let i1 : ℕ := (finProdFinEquiv.symm.toFun i).1 + 1 + let j1 : ℕ := (finProdFinEquiv.symm.toFun j).1 + 1 + rw [← ne_eq] + change i1 + i2 • h7.β ≠ j1 + j2 • h7.β + intros H + apply h7.hirr (i1 - j1) (j2 - i2) + have : i1 + i2 • h7.β = j1 + j2 • h7.β ↔ (↑i1 - ↑j1) /(↑j2 - ↑i2 : ℂ) = h7.β := by + calc _ ↔ ↑i1 - ↑j1 + ↑i2 • h7.β - ↑j2 • h7.β = 0 := ?_ + _ ↔ ↑i1 - ↑j1 + (i2 - ↑j2 : ℂ) • h7.β = 0 := ?_ + _ ↔ ↑i1 - ↑j1 = - ((i2 - ↑j2 : ℂ) • h7.β) := ?_ + _ ↔ ↑i1 - ↑j1 = (↑j2 - ↑i2 : ℂ) • h7.β := ?_ + _ ↔ (↑i1 - ↑j1) /(↑j2 - ↑i2 : ℂ) = h7.β := ?_ + · grind + · rw [sub_eq_add_neg]; simp only [nsmul_eq_mul]; rw [← neg_mul, add_assoc, ← add_mul] + simp only [smul_eq_mul];rw [← sub_eq_add_neg] + · rw [add_eq_zero_iff_eq_neg] + · refine Eq.congr_right (?_); simp only [smul_eq_mul]; rw [← neg_mul];simp only [neg_sub] + · rw [div_eq_iff, mul_comm,smul_eq_mul] + intros HC + apply (fun HC ↦ Heq (Fin.eq_of_val_eq (Nat.succ_inj.mp HC))) + rw [sub_eq_zero] at HC; simp only [Nat.cast_inj] at HC; exact HC.symm + rw [this] at H + rw [H.symm] + simp only [Int.cast_sub, Int.cast_natCast] + · exact mt + (fun h ↦ by simpa [exp_log h7.htriv.1, exp_zero] using congrArg exp h) h7.htriv.2 + +abbrev V := vandermonde (fun t ↦ h7.ρ q t) + +omit [DecidableEq (h7.K →+* ℂ)] in +lemma vandermonde_det_ne_zero : det (h7.V q) ≠ 0 := by + by_contra H + rw [V, det_vandermonde_eq_zero_iff] at H + obtain ⟨i, j, ⟨hij, hij'⟩⟩ := H + apply h7.rho_injective q i j hij' hij + +open Differentiable Complex + +abbrev R : ℂ → ℂ := fun x ↦ ∑ t, (canonicalEmbedding h7.K) + ((algebraMap (𝓞 h7.K) h7.K) ((h7.η q hq0 h2mq) t)) h7.σ * exp (h7.ρ q t * x) + +/-! +We introduce the integral function + `R(x) = η₁ e^(ρ₁ x) + … + ηₜ e^(ρₜ x)` (2) +where the coefficients `η₁, …, ηₜ` are determined by the following conditions. + + +Thus, we see from (2) that + + `R(x) = a_{n,ℓ}(x - ℓ)ⁿ + a_{n+1,ℓ}(x - ℓ)ⁿ⁺¹ + ⋯, 1 ≤ ℓ ≤ m,` (3) + +where `a_{n,ℓ}, a_{n+1,ℓ}, ...` are not all zero. Hence, there must be a natural +number `r` such that `R⁽ᵏ⁾(ℓ) = 0, 0 ≤ k ≤ r - 1, 1 ≤ ℓ ≤ m`. But for +`1 ≤ ℓ₀ ≤ m` we have `R⁽ʳ⁾(ℓ₀) ≠ 0` so that we see from (3) that `r ≥ n`. +-/ + +lemma cexp_mul (c x : ℂ) : deriv (fun x ↦ cexp (c * x)) x = c * cexp (c * x) := by + rw [deriv_cexp (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)] + simp [deriv_const', deriv_id'', mul_comm] + +def iteratedDeriv_R (k' : ℕ) : deriv^[k'] (fun x ↦ (h7.R q hq0 h2mq) x) = + fun x ↦ ∑ t, (h7.σ ((h7.η q hq0 h2mq) t)) * exp (h7.ρ q t * x) * (h7.ρ q t)^k' := by + induction k' with + | zero => simp only [pow_zero, mul_one]; rfl + | succ k hk => + rw [← iteratedDeriv_eq_iterate] at * + simp only [iteratedDeriv_succ] + conv => enter [1]; rw [hk] + ext x + rw [deriv, fderiv_fun_sum] + · simp only [ContinuousLinearMap.coe_sum', Finset.sum_apply, fderiv_eq_smul_deriv, + deriv_mul_const_field', deriv_const_mul_field', smul_eq_mul, one_mul] + rw [Finset.sum_congr rfl] + intros t ht + · rw [mul_assoc, mul_assoc, mul_eq_mul_left_iff, map_eq_zero]; left + rw [cexp_mul, mul_assoc, (pow_succ' (h7.ρ q t) k)] + · rw [mul_comm, mul_assoc, mul_eq_mul_left_iff, Eq.symm (pow_succ' (h7.ρ q t) k)]; left; rfl + · intros i hi + apply mul (by fun_prop) (differentiable_const (h7.ρ q i ^ k)) + +lemma iteratedDeriv_R_eq_zero (hR : h7.R q hq0 h2mq = 0) (z : ℂ) (k' : ℕ) : + deriv^[k'] (fun z ↦ h7.R q hq0 h2mq z) z = 0 := by + rw [hR, ← iteratedDeriv_eq_iterate, iteratedDeriv] + simp + +lemma vecMul_V_eq_zero (hR : h7.R q hq0 h2mq = 0) : + (h7.V q).vecMul (fun t ↦ h7.σ ((h7.η q hq0 h2mq) t)) = 0 := by + ext k + have hk : deriv^[k] (fun x ↦ h7.R q hq0 h2mq x) 0 = 0 := + h7.iteratedDeriv_R_eq_zero (hR := hR) _ _ _ _ _ + rw [h7.iteratedDeriv_R q hq0 h2mq k] at hk + simpa [of_apply] using hk + +lemma ηvec_eq_zero (hVecMulEq0 : (h7.V q).vecMul (fun t ↦ h7.σ ((h7.η q hq0 h2mq) t)) = 0) : + (fun t ↦ h7.σ ((h7.η q hq0 h2mq) t )) = 0 := by + apply eq_zero_of_vecMul_eq_zero + (h7.vandermonde_det_ne_zero q) hVecMulEq0 + +lemma hbound_sigma : h7.η q hq0 h2mq ≠ 0 := + (house.exists_ne_zero_int_vec_house_le h7.K (h7.A q) + (h7.hM_ne_zero q hq0 h2mq) (mul_pos (Nat.zero_lt_succ (2 * h7.h + 1)) + (h7.one_le_n q hq0 h2mq)) (h7.m_mul_n_lt_q_mul_q q hq0 h2mq) (Fintype.card_fin _) + (fun u t ↦ h7.house_matrixA_le q hq0 u t h2mq) (Fintype.card_fin _)).choose_spec.1 + +lemma R_ne_zero : h7.R q hq0 h2mq ≠ 0 := by + intro H + have HC := ηvec_eq_zero h7 q hq0 h2mq (vecMul_V_eq_zero h7 q hq0 h2mq H) + apply hbound_sigma h7 q hq0 h2mq + ext t + simpa [η, FaithfulSMul.algebraMap_eq_zero_iff] using congr_fun HC t + +variable (hγ : h7.α ^ h7.β = h7.σ h7.γ') + +omit [DecidableEq (h7.K →+* ℂ)] in +lemma systemCoeffs_map_eq_exp_mul : + Complex.exp (h7.ρ q t * h7.l q u) * (h7.ρ q t ^ (h7.k q u : ℕ) * + Complex.log h7.α ^ (-(h7.k q u) : ℤ)) = h7.σ (h7.systemCoeffs q u t) := by + calc _ = cexp (h7.ρ q t * h7.l q u) * (((↑(a q t) + ↑(b q t) • h7.β) * + Complex.log h7.α) ^ (h7.k q u : ℕ) * Complex.log h7.α ^ (-↑(h7.k q u) : ℤ)) := ?_ + _ = cexp (h7.ρ q t * h7.l q u) * ((↑(a q t) + ↑(b q t) • h7.β) ^ (h7.k q u : ℕ) * + ((Complex.log h7.α) ^ (h7.k q u : ℕ) * Complex.log h7.α ^ (-(h7.k q u) : ℤ))) := ?_ + _ = cexp (h7.ρ q t * h7.l q u) * ((↑(a q t) + ↑(b q t) • h7.β) ^ (h7.k q u : ℕ)) := ?_ + _ = h7.σ (h7.systemCoeffs q u t) := ?_ + · nth_rw 2 [ρ] + · rw [mul_pow, mul_assoc] + · have h_log_ne : Complex.log h7.α ≠ 0 := + mt (fun h ↦ by simpa [exp_log h7.htriv.1, exp_zero] using congrArg Complex.exp h) h7.htriv.2 + aesop + · rw [h7.habc.2.1, mul_comm, systemCoeffs, mul_assoc] + simp only [nsmul_eq_mul, map_pow, map_add, map_natCast, map_mul, mul_eq_mul_left_iff, + pow_eq_zero_iff', ne_eq]; left + rw [← h7.habc.1, ← h7.habc.2.2, ρ, ← cpow_nat_mul] + have : h7.α ^ ((a q t * h7.l q u)) * h7.α ^ (↑(b q t * h7.l q u) * h7.β) = + h7.α ^ ((a q t * h7.l q u) + (↑(b q t * h7.l q u) * h7.β)) := by + rw [cpow_add _ _ h7.htriv.1] + · rw [cpow_nat_mul] + simp only [mul_eq_mul_right_iff, pow_eq_zero_iff', cpow_eq_zero_iff, ne_eq, mul_eq_zero, + not_or]; left; rw [cpow_nat_mul, cpow_natCast]; exact pow_mul' h7.α (a q t) (h7.l q u) + rw [this]; clear this + · rw [cpow_def_of_ne_zero h7.htriv.1 _] + · congr 1; rw [mul_rotate, mul_assoc]; simp only [nsmul_eq_mul, Nat.cast_mul] + nth_rw 3 [mul_comm]; rw [mul_assoc]; grind + +include hq0 h2mq in +lemma systemCoeffs_deriv : + (Complex.log h7.α)^(-(h7.k q u) : ℤ) * deriv^[h7.k q u] (h7.R q hq0 h2mq) (h7.l q u) = + ∑ t, h7.σ ↑((h7.η q hq0 h2mq) t) * h7.σ (h7.systemCoeffs q u t) := by + rw [iteratedDeriv_R, mul_sum, Finset.sum_congr rfl] + intros t ht + rw [mul_assoc, mul_comm, mul_assoc] + simp only [mul_eq_mul_left_iff, map_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] + left + have := systemCoeffs_map_eq_exp_mul h7 q u t + unfold l at this + rw [mul_assoc] + unfold l + exact this + +lemma coeffs_mulVec_A_eq : h7.σ (h7.c_coeffs q) * ((Complex.log h7.α)^ (-(h7.k q u) : ℤ) * + deriv^[h7.k q u] (h7.R q hq0 h2mq) (h7.l q u)) = h7.σ ((h7.A q *ᵥ (h7.η q hq0 h2mq)) u) := by + rw [systemCoeffs_deriv h7 q hq0 u h2mq] + unfold Matrix.mulVec dotProduct + simp only [← map_mul, ← map_sum] + congr 1 + rw [Finset.mul_sum] + simp only [Int.cast_mul, Int.cast_pow, map_sum, map_mul] + apply Finset.sum_congr rfl + intros x hx + simp only [A, RingOfIntegers.restrict, zsmul_eq_mul, RingOfIntegers.map_mk] + push_cast + ring + +lemma coeffs_mul_deriv_eq_zero : h7.σ (h7.c_coeffs q) * ((Complex.log h7.α)^ (-(h7.k q u) : ℤ) * + deriv^[h7.k q u] (h7.R q hq0 h2mq) (h7.l q u)) = 0 := by + rw [coeffs_mulVec_A_eq] + have hMt0 := (NumberField.house.exists_ne_zero_int_vec_house_le h7.K (h7.A q) + (hM_ne_zero h7 q hq0 h2mq) (mul_pos ((Nat.zero_lt_succ (2 * h7.h + 1))) + (h7.one_le_n q hq0 h2mq)) (h7.m_mul_n_lt_q_mul_q q hq0 h2mq) (Fintype.card_fin _) + (fun u t ↦ house_matrixA_le h7 q hq0 u t h2mq) (Fintype.card_fin _)).choose_spec.2.1 + simp [η, FaithfulSMul.algebraMap_eq_zero_iff] + aesop + +/-!After defining the auxiliary function R we consider the +first nonzero derivative at an integer ℓ₀. + + `(log α)⁻ʳ R⁽ʳ⁾(ℓ₀) = ρ`. + +where r is the smallest integer such that `R⁽ʳ⁾(ℓ₀) ≠ 0`.-/ + +lemma exists_min_analyticOrderAt : + let s : Finset (Fin (h7.m)) := Finset.univ + ∃ l₀' ∈ s, (∃ y, (analyticOrderAt (h7.R q hq0 h2mq) (l₀' + 1)) = y ∧ + (∀ (l' : Fin (h7.m)), l' ∈ s → y ≤ (analyticOrderAt (h7.R q hq0 h2mq) (l' + 1)))) := by + intro s + obtain ⟨x, hx, hmin⟩ := Finset.exists_min_image s + (fun x ↦ analyticOrderAt (h7.R q hq0 h2mq) (x + 1)) + ⟨⟨0, Nat.zero_lt_succ (2 * h7.h + 1)⟩, Finset.mem_univ _⟩ + exact ⟨x, hx, _, rfl, hmin⟩ + +abbrev l₀' : Fin (h7.m) := (exists_min_analyticOrderAt h7 q hq0 h2mq).choose + +abbrev l₀_prop := (exists_min_analyticOrderAt h7 q hq0 h2mq).choose_spec.2 + +abbrev r' := (l₀_prop h7 q hq0 h2mq).choose + +lemma r'_spec : + let s : Finset (Fin (h7.m)) := Finset.univ + analyticOrderAt (h7.R q hq0 h2mq) ↑↑(h7.l₀' q hq0 h2mq + 1 : ℂ) = + h7.r' q hq0 h2mq ∧ ∀ l' ∈ s, h7.r' q hq0 h2mq ≤ analyticOrderAt (h7.R q hq0 h2mq) (↑↑l' + 1) := + (h7.l₀_prop q hq0 h2mq).choose_spec + +end Setup +end diff --git a/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainPostAnalytic.lean b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainPostAnalytic.lean new file mode 100644 index 00000000000000..629e7617a908b5 --- /dev/null +++ b/Mathlib/NumberTheory/Transcendental/GelfondSchneider/MainPostAnalytic.lean @@ -0,0 +1,378 @@ +/- +Copyright (c) 2026 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ + +module + +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAnalytic +public import Mathlib.NumberTheory.Transcendental.GelfondSchneider.AnalyticPart + +@[expose] public section + +open BigOperators Module.Free Fintype NumberField Embeddings FiniteDimensional + Matrix Set Polynomial Finset IntermediateField Complex AnalyticAt + +noncomputable section + +variable (h7 : Setup) (q : ℕ) (hq0 : 0 < q) (u : Fin (h7.m * h7.n q)) + (t : Fin (q * q)) [DecidableEq (h7.K →+* ℂ)] (h2mq : 2 * h7.m ∣ q ^ 2) + +open Set AnalyticAt AnalyticOnNhd + + +namespace Setup + +lemma exists_nonzero_iteratedFDeriv : deriv^[h7.r q hq0 h2mq] + (h7.R q hq0 h2mq) (h7.l₀' q hq0 h2mq + 1) ≠ 0 := by + have Hrprop := (h7.r_prop q hq0 h2mq).1 + obtain ⟨l₀, y, r, h1, h2⟩ := (h7.exists_min_analyticOrderAt q hq0 h2mq) + have hA1 : AnalyticAt ℂ (h7.R q hq0 h2mq) (↑↑(h7.l₀' q hq0 h2mq) + 1) := by fun_prop + grind [analyticOrderAt_eq_nat_imp_iteratedDeriv_eq_zero hA1] + +lemma ρᵣ_nonzero : ρᵣ h7 q hq0 h2mq ≠ 0 := by + unfold ρᵣ + simp only [zpow_neg, zpow_natCast, mul_eq_zero, inv_eq_zero, + pow_eq_zero_iff', ne_eq, not_or, not_and, Decidable.not_not] + refine ⟨fun hlog => ?_, h7.exists_nonzero_iteratedFDeriv q hq0 h2mq⟩ + · by_contra H + have : Complex.log h7.α ≠ 0 := + mt (fun h ↦ by simpa [exp_log h7.htriv.1, exp_zero] using congrArg exp h) h7.htriv.2 + apply this; exact hlog + +lemma rho_nonzero : rho h7 q hq0 h2mq ≠ 0 := by + intros H + apply_fun h7.σ at H + rw [rho_eq_ρᵣ] at H + simp only [map_zero] at H + apply h7.ρᵣ_nonzero + exact H + +lemma norm_Algebra_norm_rho_nonzero : + ‖(Algebra.norm ℚ) (rho h7 q hq0 h2mq)‖ ≠ 0 := by + rw [norm_ne_zero_iff, Algebra.norm_ne_zero_iff] + intros H + apply_fun h7.σ at H + rw [rho_eq_ρᵣ] at H + simp only [map_zero] at H + apply ρᵣ_nonzero h7 q hq0 h2mq + exact H + +lemma c1rho_neq_0 : h7.c1ρ q hq0 h2mq ≠ 0 := by + intros H + injection H with H1 + simp only [zsmul_eq_mul, mul_eq_zero, Int.cast_eq_zero] at H1 + cases H1 with + | inl hp => apply cρ_ne_zero h7 q hq0 h2mq; exact hp + | inr hq => + apply_fun h7.σ at hq + rw [rho_eq_ρᵣ] at hq + simp only [map_zero] at hq + apply ρᵣ_nonzero h7 q hq0 h2mq + exact hq + +lemma house_geq_1 : 1 ≤ house (h7.c1ρ q hq0 h2mq : h7.K) := by + apply one_le_house_of_isIntegral (RingOfIntegers.isIntegral_coe (h7.c1ρ q hq0 h2mq)) + simp only [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff] + rw [← ne_eq] + exact c1rho_neq_0 h7 q hq0 h2mq + +lemma eq5zero : 1 ≤ norm + (Algebra.norm ℚ ((algebraMap (𝓞 h7.K) h7.K) (h7.c1ρ q hq0 h2mq))) := by + have := ρ_is_int h7 q hq0 h2mq + have := Algebra.isIntegral_norm ℚ this + have H1 : 0 ≤ ‖(Algebra.norm ℤ) (h7.c1ρ q hq0 h2mq)‖ := by + positivity + have H2 : 0 ≠ ‖(Algebra.norm ℤ) (h7.c1ρ q hq0 h2mq)‖ := by + have := c1rho_neq_0 h7 q hq0 h2mq + symm + intros H + apply this + rw [norm_eq_zero] at H + simp only [Algebra.norm_eq_zero_iff] at H + exact H + have : 0 < ‖(Algebra.norm ℤ) (h7.c1ρ q hq0 h2mq)‖ := by + exact lt_of_le_of_ne H1 H2 + rw [← Algebra.coe_norm_int] at * + simp only [Int.norm_cast_rat, ge_iff_le] at * + rw [← Int.norm_cast_real] at * + simp only [Real.norm_eq_abs] at * + norm_cast at * + +def c₅ : ℝ := ((abs (h7.c₁) + 1) ^ (((↑(h7.h) * (1+4 * h7.m^2))))) + +omit [DecidableEq (h7.K →+* ℂ)] in +lemma c5nonneg : 0 < h7.c₅ := by + unfold c₅ + apply pow_pos + simp only [Int.cast_abs] + refine add_pos_of_nonneg_of_pos ?_ ?_ + · simp only [abs_nonneg] + · simp only [zero_lt_one] + +------ +lemma order_geq_n_foo (l' : Fin (h7.m)) : + (∀ k', k' < h7.n q → deriv^[k'] (h7.R q hq0 h2mq) (l' + 1) = 0) + → h7.n q ≤ analyticOrderAt (h7.R q hq0 h2mq) (l' + 1) := by + intros H + apply le_analyticOrderAt_iff_iteratedDeriv_eq_zero + · fun_prop + · apply order_neq_top h7 q hq0 h2mq l' + exact H + +lemma order_geq_n : ∀ l' : Fin (h7.m), + h7.n q ≤ analyticOrderAt (h7.R q hq0 h2mq) (l' + 1) := by + intros l' + apply order_geq_n_foo + intros k hk + have H := h7.iteratedkDeriv_R_eq_zero q hq0 h2mq ⟨k,hk⟩ l' + rw [H] + +lemma n_le_r : h7.n q ≤ h7.r q hq0 h2mq := by + have := h7.r_prop q hq0 h2mq + obtain ⟨hr,hprop⟩ := this + have := h7.order_geq_n q hq0 h2mq (h7.l₀' q hq0 h2mq) + have H : h7.n q ≤ (h7.r q hq0 h2mq : ℕ∞) → h7.n q ≤ h7.r q hq0 h2mq := by + simp only [Nat.cast_le, imp_self] + apply H + rw [← hr] + apply this + +lemma r_ne_zero : h7.r q hq0 h2mq ≠ 0 := by + have H := n_le_r h7 q hq0 h2mq + have : 0 < h7.n q := by + unfold n; simp only [Nat.div_pos_iff, Nat.ofNat_pos, + mul_pos_iff_of_pos_left] + refine ⟨Nat.zero_lt_succ (2 * h7.h + 1), Nat.le_of_dvd (Nat.pow_pos hq0) h2mq⟩ + aesop + +/-!so that + +$$ +|N(\rho)| > c_1^{-h(r+2mq)} > c_5^{-r}. +$$-/ + +lemma eq5 : h7.c₅ ^ (-(h7.r q hq0 h2mq) : ℝ) < norm (Algebra.norm ℚ (rho h7 q hq0 h2mq)) := by + simp only [Real.rpow_neg_natCast, zpow_neg, zpow_natCast] + have h1 : 1 ≤ ‖(h7.cρ q hq0 h2mq) ^ Module.finrank ℚ h7.K‖ * + ‖(Algebra.norm ℚ) (rho h7 q hq0 h2mq)‖ := by + have := eq5zero h7 q hq0 h2mq + unfold c1ρ at this + unfold RingOfIntegers.restrict at this + simp only [zsmul_eq_mul] at this + simp only [RingOfIntegers.map_mk, map_mul, norm_mul] at this + have H := @Algebra.norm_algebraMap ℚ _ h7.K _ _ (h7.cρ q hq0 h2mq) + simp only [map_intCast] at H + simp only [norm_pow, ge_iff_le] + rw [H] at this + simp only [norm_pow, Int.norm_cast_rat] at this + exact this + have h2 : ‖(h7.cρ q hq0 h2mq) ^ Module.finrank ℚ h7.K‖⁻¹ + ≤ norm (Algebra.norm ℚ (rho h7 q hq0 h2mq)) := by + have : 0 < ‖ (h7.cρ q hq0 h2mq)^ Module.finrank ℚ h7.K‖ := by + rw [norm_pos_iff] + simp only [ne_eq, pow_eq_zero_iff', not_and, Decidable.not_not] + intros H + by_contra H1 + apply h7.cρ_ne_zero q hq0 h2mq + exact H + rw [← mul_le_mul_iff_right₀ this] + · rw [mul_inv_cancel₀] + · simp_all only [norm_pow] + · simp only [norm_pow, ne_eq, pow_eq_zero_iff', norm_eq_zero, + not_and, Decidable.not_not] + intros H + rw [H] at this + simp only [norm_pow, norm_zero] at this + rw [zero_pow] at this + · by_contra H1 + simp_all only [norm_pow, lt_self_iff_false] + · simp_all only [norm_pow] + have : 0 < Module.finrank ℚ h7.K := by + exact Module.finrank_pos + simp_all only [norm_zero, ne_eq] + apply Aesop.BuiltinRules.not_intro + intro a + simp_all only [pow_zero, one_mul, zero_lt_one, lt_self_iff_false] + calc _ = _ := ?_ + h7.c₅ ^ ((-h7.r q hq0 h2mq : ℤ)) < + abs (h7.c₁)^ ((- h7.h : ℤ) * (h7.r q hq0 h2mq + 2 * h7.m * q) ) := ?_ + _ ≤ ‖(h7.cρ q hq0 h2mq) ^ Module.finrank ℚ h7.K‖⁻¹ := ?_ + _ ≤ norm (Algebra.norm ℚ (rho h7 q hq0 h2mq)) := ?_ + · simp only [zpow_neg, zpow_natCast] + · simp only [zpow_neg, zpow_natCast, neg_mul] + rw [inv_lt_inv₀] + · rw [mul_add] + have : (h7.h : ℤ) * h7.r q hq0 h2mq + h7.h + * (2 * h7.m * ↑q) = h7.h * h7.r q hq0 h2mq + h7.h * 2 * h7.m * ↑q := by + rw [mul_assoc, mul_assoc, mul_assoc] + rw [this] + have : ((h7.h : ℤ) * h7.r q hq0 h2mq + ↑(h7.h) * 2 * ↑(h7.m) * ↑q) = + ((h7.h : ℤ) * (↑(h7.r q hq0 h2mq) + 2 * ↑(h7.m) * ↑q)) := + Eq.symm (Mathlib.Tactic.Ring.mul_add rfl rfl this) + rw [this] + dsimp [c₅] + norm_cast + nth_rw 2 [pow_mul] + have : (((abs (h7.c₁) + 1) ^ h7.h) ^ (1 + 4 * h7.m ^ 2)) ^ h7.r q hq0 h2mq= + ((abs (h7.c₁) + 1) ^ (h7.h * (1 + 4 * h7.m ^ 2) * h7.r q hq0 h2mq)) := by + rw [pow_mul] + rw [pow_mul] + rw [this]; clear this + calc _ ≤ abs (h7.c₁) ^ (h7.h * (h7.r q hq0 h2mq + 2 * h7.m * q^2)):= ?_ + _ ≤ abs (h7.c₁) ^ (h7.h * (h7.r q hq0 h2mq + 4 * h7.m ^ 2 * h7.n q)) := ?_ + _ ≤ abs (h7.c₁) ^( h7.h * (1 + 4 * h7.m ^ 2) * h7.r q hq0 h2mq) := ?_ + _ < (abs (h7.c₁) + 1) ^ (h7.h * (1 + 4 * h7.m ^ 2) * h7.r q hq0 h2mq) := ?_ + · refine pow_le_pow_right₀ ?_ ?_ + · exact one_le_abs_c₁ h7 + · simp only [mul_assoc] + refine Nat.mul_le_mul (le_refl _) ?_ + · rw [q_sq_eq_two_mn h7 q h2mq] + simp only [add_le_add_iff_left, Nat.ofNat_pos, mul_le_mul_iff_right₀] + refine Nat.mul_le_mul (le_refl _) ?_ + · trans + · have : q ≤ q^2 := by + refine Nat.le_pow ?_ + simp only [Nat.ofNat_pos] + apply this + · rw [q_sq_eq_two_mn h7 q h2mq] + · simp only [mul_assoc] + refine pow_le_pow_right₀ ?_ ?_ + · exact one_le_abs_c₁ h7 + · refine Nat.mul_le_mul (le_refl _) ?_ + · rw [q_sq_eq_two_mn h7 q h2mq] + simp only [add_le_add_iff_left] + have : 2 * (h7.m * (2 * h7.m * h7.n q))= + 4 * h7.m ^ 2 * h7.n q := by + rw [mul_assoc, mul_assoc] + ring + rw [this] + simp only [mul_assoc,le_refl] + · rw [mul_add] + rw [mul_add] + rw [add_mul] + simp only [mul_one] + refine pow_le_pow_right₀ ?_ ?_ + · exact one_le_abs_c₁ h7 + · simp only [add_le_add_iff_left] + simp only [mul_assoc] + refine Nat.mul_le_mul (le_refl _) ?_ + · simp only [Nat.ofNat_pos, mul_le_mul_iff_right₀] + refine Nat.mul_le_mul (le_refl _) ?_ + · exact n_le_r h7 q hq0 h2mq + · refine pow_lt_pow_left₀ ?_ ?_ ?_ + · simp only [lt_add_iff_pos_right, zero_lt_one] + · simp only [abs_nonneg] + · intros H + simp only [mul_eq_zero, Nat.add_eq_zero_iff, + one_ne_zero, OfNat.ofNat_ne_zero, + Nat.pow_eq_zero, ne_eq, not_false_eq_true, and_true, + false_or, false_and, or_false] at H + rcases H with h1 | h2 + · have : 0 ≠ h7.h := by + symm ;apply Nat.pos_iff_ne_zero.mp + dsimp [h] + exact Module.finrank_pos + apply this + exact h1.symm + · apply r_ne_zero h7 q hq0 h2mq + exact h2 + · unfold c₅ + trans + · have : (0 : ℝ) < 1 := by simp only [zero_lt_one] + apply this + · apply one_lt_pow₀ + · refine one_lt_pow₀ ?_ ?_ + · simp only [Int.cast_abs, lt_add_iff_pos_left, abs_pos, ne_eq, Int.cast_eq_zero] + rw [← ne_eq] + exact c₁_ne_zero h7 + · simp only [ne_eq, mul_eq_zero, Nat.add_eq_zero_iff, one_ne_zero, OfNat.ofNat_ne_zero, + Nat.pow_eq_zero, not_false_eq_true, and_true, false_or, false_and, or_false] + · unfold h + have : 0 < Module.finrank ℚ h7.K := Module.finrank_pos + simp_all only [norm_pow, ne_eq] + apply Aesop.BuiltinRules.not_intro + intro a + simp_all only [pow_zero, one_mul, inv_one, lt_self_iff_false] + · exact r_ne_zero h7 q hq0 h2mq + · have : 1 ≤ abs (h7.c₁) ^ (↑(h7.h) * + ((↑(h7.r q hq0 h2mq)) + 2 * ↑(h7.m) * (↑q))) := by + refine one_le_pow₀ ?_ + have : 1 ≤ h7.c₁ := h7.one_le_c₁ + exact one_le_abs_c₁ h7 + calc (0 : ℝ) < 1 := by simp only [zero_lt_one] + (1 : ℝ) ≤ abs (h7.c₁) ^ (↑(h7.h) * + ((↑(h7.r q hq0 h2mq)) + 2 * ↑(h7.m) * (↑q))) := mod_cast this + · unfold cρ + simp only [neg_mul, zpow_neg] + simp only [Int.cast_abs, norm_pow] + rw [Int.norm_eq_abs] + simp only [Int.cast_abs, Int.cast_mul, Int.cast_pow, abs_abs] + rw [← abs_pow] + rw [← Real.rpow_natCast] + rw [← Real.rpow_natCast] + rw [← Real.rpow_natCast] + rw [← Real.rpow_add] + · rw [← Real.rpow_mul] + · rw [mul_comm] + norm_cast + simp only [Int.cast_pow, Int.cast_abs, abs_pow] + unfold h + simp only [le_refl] + · exact mod_cast (le_trans Int.one_nonneg (h7.one_le_c₁)) + · rw [lt_iff_le_and_ne] + refine ⟨mod_cast (le_trans Int.one_nonneg (h7.one_le_c₁)), fun H ↦ ?_⟩ + · apply c₁_ne_zero h7 + symm + exact mod_cast H + · exact h2 + +lemma c_coeffspow_r : + ((h7.c₁) ^ (h7.r q hq0 h2mq) * (h7.c₁) ^ (h7.m * q) * (h7.c₁) ^ (h7.m * q)) = + ((h7.c₁) ^ ((h7.r q hq0 h2mq)) * + (h7.c₁) ^ (h7.m * q - (a q t * (↑(h7.l₀' q hq0 h2mq) + 1))) * + (h7.c₁) ^ (h7.m * q - ((b q t * (↑(h7.l₀' q hq0 h2mq) + 1))))) • + (h7.c₁) ^ (a q t * (↑(h7.l₀' q hq0 h2mq) + 1)) * + (h7.c₁) ^ (b q t * (↑(h7.l₀' q hq0 h2mq) + 1)) := by + rw [← one_mul (h7.c₁ ^ (a q t * (↑(h7.l₀' q hq0 h2mq : ℕ) + 1)))] + have triple_comm_int (a b c : ℤ) (x y z : ℤ) : + ((a*b)*c) • ((x*y)*z) = a•x * b•y * c•z := by + simp only [zsmul_eq_mul, Int.cast_mul]; ring + simp only [mul_assoc] + rw [ smul_mul_assoc + (h7.c₁ ^ h7.r q hq0 h2mq * + (h7.c₁ ^ (h7.m * q - a q t * (↑(h7.l₀' q hq0 h2mq) + 1)) * + h7.c₁ ^ (h7.m * q - b q t * (↑(h7.l₀' q hq0 h2mq) + 1)))) + (1 * h7.c₁ ^ (a q t * (↑(h7.l₀' q hq0 h2mq) + 1))) + (h7.c₁ ^ (b q t * (↑(h7.l₀' q hq0 h2mq) + 1)))] + rw [Int.mul_assoc 1 (h7.c₁ ^ (a q t * (↑(h7.l₀' q hq0 h2mq) + 1))) + (h7.c₁ ^ (b q t * (↑(h7.l₀' q hq0 h2mq) + 1)))] + simp only [← mul_assoc] + rw [triple_comm_int] + congr + · simp only [Int.zsmul_eq_mul, mul_one] + · simp only [smul_eq_mul] + rw [← pow_add] + have : (h7.m * q - (a q t * (↑(h7.l₀' q hq0 h2mq) + 1)) + + (a q t * (↑(h7.l₀' q hq0 h2mq) + 1))) = (h7.m * q) := by + rw [add_comm] + refine add_tsub_cancel_of_le ?_ + rw [mul_comm h7.m] + apply mul_le_mul (((finProdFinEquiv.symm.toFun t).1).isLt) ?_ (zero_le _) (zero_le _) + · exact (h7.l₀' q hq0 h2mq).isLt + rw [this] + · simp only [smul_eq_mul] + rw [← pow_add] + have : (h7.m * q - (b q t * (↑(h7.l₀' q hq0 h2mq) + 1)) + + (b q t * (↑(h7.l₀' q hq0 h2mq) + 1))) = (h7.m * q) := by + rw [add_comm] + refine add_tsub_cancel_of_le ?_ + rw [mul_comm h7.m] + apply mul_le_mul (((finProdFinEquiv.symm.toFun t).2).isLt) ?_ (zero_le _) (zero_le _) + · exact (h7.l₀' q hq0 h2mq).isLt + rw [this] + +end Setup + +end