From 087b85ebb641d31f3de0bf16fb1d8d02bc3b3fba Mon Sep 17 00:00:00 2001 From: rbajaj5 Date: Fri, 24 Jul 2026 00:26:51 -0400 Subject: [PATCH 1/3] Develop Fourier bounds for Shunia conjecture --- Mathlib/NumberTheory/Shunia.lean | 684 +++++++++++++++++++++++++++++++ 1 file changed, 684 insertions(+) create mode 100644 Mathlib/NumberTheory/Shunia.lean diff --git a/Mathlib/NumberTheory/Shunia.lean b/Mathlib/NumberTheory/Shunia.lean new file mode 100644 index 00000000000000..e5b5f2e1df19dc --- /dev/null +++ b/Mathlib/NumberTheory/Shunia.lean @@ -0,0 +1,684 @@ +/- +Copyright (c) 2026 rbajaj5. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: rbajaj5 +-/ +module + +public import Mathlib.Analysis.Fourier.ZMod +public import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds +public import Mathlib.Algebra.BigOperators.ModEq +public import Mathlib.Data.Nat.Log +public import Mathlib.Tactic + +/-! +# Shunia's integer-root formula + +This file develops the coefficient and Fourier estimates needed to formalize Conjecture 6.1 +from Joseph M. Shunia, +*Polynomial quotient rings and Kronecker substitution for deriving combinatorial identities*. + +The intended public statement will be phrased using `Nat.nthRoot`: the quotient of the two least +nonnegative residues is one more than the integer `n`-th root. +-/ + +public section + +namespace Nat + +open scoped BigOperators + +/-- The base used for the Kronecker substitution in Shunia's formula. -/ +def shuniaBase (a n : ℕ) : ℕ := a ^ (2 * a * n) + +/-- The modulus used in Shunia's formula. -/ +def shuniaModulus (a n : ℕ) : ℕ := shuniaBase a n ^ n - a + +/-- The denominator residue in Shunia's formula. -/ +def shuniaDenominator (a n : ℕ) : ℕ := + (shuniaBase a n + 1) ^ (2 * a * n) % shuniaModulus a n + +/-- The numerator residue in Shunia's formula. -/ +def shuniaNumerator (a n : ℕ) : ℕ := + (shuniaBase a n + 1) ^ (2 * a * n + 1) % shuniaModulus a n + +/-- The coefficient of residue class `i` in the reduction of `(1 + T) ^ k` modulo `T ^ n - a`. -/ +def shuniaCoeff (a n k : ℕ) (i : ZMod n) : ℕ := + ∑ j ∈ Finset.range (k + 1), + if (j : ZMod n) = i then k.choose j * a ^ (j / n) else 0 + +/-- Evaluation at `X` of the reduced coefficient vector for `(1 + T) ^ k`. -/ +def shuniaCoeffEval (a n k X : ℕ) [NeZero n] : ℕ := + ∑ i : ZMod n, shuniaCoeff a n k i * X ^ i.val + +private lemma shuniaCoeffEval_eq_sum (a n k X : ℕ) [NeZero n] : + shuniaCoeffEval a n k X = + ∑ j ∈ Finset.range (k + 1), k.choose j * a ^ (j / n) * X ^ (j % n) := by + classical + simp only [shuniaCoeffEval, shuniaCoeff, Finset.sum_mul] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro j hj + simp [eq_comm, ZMod.val_natCast] + +private lemma pow_modEq_div_mod (a n X j : ℕ) (haX : a ≤ X ^ n) : + X ^ j ≡ a ^ (j / n) * X ^ (j % n) [MOD X ^ n - a] := by + have hbase : X ^ n ≡ a [MOD X ^ n - a] := + ((Nat.modEq_iff_dvd' haX).2 dvd_rfl).symm + calc + X ^ j = X ^ (n * (j / n) + j % n) := by + congr 1 + simpa [mul_comm] using (Nat.div_add_mod' j n).symm + _ = (X ^ n) ^ (j / n) * X ^ (j % n) := by rw [pow_add, pow_mul] + _ ≡ a ^ (j / n) * X ^ (j % n) [MOD X ^ n - a] := + (hbase.pow (j / n)).mul_right _ + +private lemma pow_add_one_modEq_coeffEval (a n k X : ℕ) [NeZero n] (haX : a ≤ X ^ n) : + (X + 1) ^ k ≡ shuniaCoeffEval a n k X [MOD X ^ n - a] := by + rw [shuniaCoeffEval_eq_sum] + have hsum := Nat.ModEq.sum (s := Finset.range (k + 1)) fun j _ ↦ + (pow_modEq_div_mod a n X j haX).mul_left (k.choose j) + simpa [add_pow, mul_assoc, mul_comm, mul_left_comm] using hsum + +private noncomputable def shuniaScaledCoeff (a n k : ℕ) (α : ℝ) (i : ZMod n) : ℂ := + shuniaCoeff a n k i * (α : ℂ) ^ i.val + +private lemma cast_pow_div_mul_pow_mod {a n j : ℕ} {α : ℝ} (hα : α ^ n = a) : + ((a ^ (j / n) : ℕ) : ℂ) * (α : ℂ) ^ (j % n) = (α : ℂ) ^ j := by + have hαc : (α : ℂ) ^ n = (a : ℂ) := by exact_mod_cast hα + rw [Nat.cast_pow, ← hαc, ← pow_mul, ← pow_add] + congr 1 + simpa [mul_comm] using Nat.div_add_mod' j n + +private lemma stdAddChar_neg_natCast_mul (n j : ℕ) [NeZero n] (t : ZMod n) : + ZMod.stdAddChar (-((j : ZMod n) * t)) = ZMod.stdAddChar (-t) ^ j := by + rw [show -((j : ZMod n) * t) = j • (-t) by simp [nsmul_eq_mul]] + exact AddChar.map_nsmul_eq_pow (ZMod.stdAddChar (N := n)) j (-t) + +private lemma dft_shuniaScaledCoeff (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) + (t : ZMod n) : + ZMod.dft (shuniaScaledCoeff a n k α) t = + (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by + classical + rw [ZMod.dft_apply] + simp only [shuniaScaledCoeff, shuniaCoeff, smul_eq_mul, Nat.cast_sum, Nat.cast_ite, + Nat.cast_mul, Nat.cast_pow, Nat.cast_zero] + conv_lhs => + enter [2, i] + rw [← mul_assoc, Finset.mul_sum, Finset.sum_mul] + rw [Finset.sum_comm] + calc + _ = ∑ j ∈ Finset.range (k + 1), + (k.choose j : ℂ) * ((α : ℂ) * ZMod.stdAddChar (-t)) ^ j := by + apply Finset.sum_congr rfl + intro j hj + simp only [mul_ite, ite_mul, mul_zero, zero_mul, eq_comm, Fintype.sum_ite_eq'] + rw [ZMod.val_natCast, stdAddChar_neg_natCast_mul] + have hpower : + (a : ℂ) ^ (j / n) * (α : ℂ) ^ (j % n) = (α : ℂ) ^ j := by + simpa only [Nat.cast_pow] using + (cast_pow_div_mul_pow_mod (a := a) (n := n) (j := j) hα) + rw [show ZMod.stdAddChar (-t) ^ j * + ((k.choose j : ℂ) * (a : ℂ) ^ (j / n)) * (α : ℂ) ^ (j % n) = + (k.choose j : ℂ) * ZMod.stdAddChar (-t) ^ j * + ((a : ℂ) ^ (j / n) * (α : ℂ) ^ (j % n)) by ring, + hpower, mul_pow] + ring + _ = (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by + simpa [mul_comm, add_comm] using + (add_pow ((α : ℂ) * ZMod.stdAddChar (-t)) 1 k).symm + +private lemma shuniaScaledCoeff_eq_fourierSum + (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) : + shuniaScaledCoeff a n k α i = + (n : ℂ)⁻¹ * ∑ t : ZMod n, + ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by + have hinv := + congrFun ((ZMod.dft (N := n) (E := ℂ)).symm_apply_apply + (shuniaScaledCoeff a n k α)) i + rw [ZMod.invDFT_apply] at hinv + simpa only [smul_eq_mul, dft_shuniaScaledCoeff a n k α hα] using hinv.symm + +/-- The positive real contribution of the trivial character in the Fourier formula. -/ +private noncomputable def shuniaMainTerm (n k : ℕ) (α : ℝ) : ℂ := + (n : ℂ)⁻¹ * (1 + (α : ℂ)) ^ k + +private lemma shuniaScaledCoeff_sub_mainTerm + (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) : + shuniaScaledCoeff a n k α i - shuniaMainTerm n k α = + (n : ℂ)⁻¹ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by + rw [shuniaScaledCoeff_eq_fourierSum a n k α hα, shuniaMainTerm] + rw [← Finset.add_sum_erase Finset.univ + (fun t : ZMod n ↦ + ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k) + (Finset.mem_univ (0 : ZMod n))] + simp + ring + +private lemma norm_shuniaScaledCoeff_sub_mainTerm_le_sum + (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) : + ‖shuniaScaledCoeff a n k α i - shuniaMainTerm n k α‖ ≤ + ‖(n : ℂ)⁻¹‖ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k := by + rw [shuniaScaledCoeff_sub_mainTerm a n k α hα, norm_mul] + gcongr + calc + ‖∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k‖ + ≤ ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖ZMod.stdAddChar (t * i) * + (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k‖ := norm_sum_le _ _ + _ = ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k := by + apply Finset.sum_congr rfl + intro t ht + simp [norm_pow] + +private lemma norm_shuniaScaledCoeff_sub_mainTerm_le + (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) (B : ℝ) + (hB : ∀ t : ZMod n, t ≠ 0 → ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ≤ B) : + ‖shuniaScaledCoeff a n k α i - shuniaMainTerm n k α‖ ≤ + ‖(n : ℂ)⁻¹‖ * ((n - 1 : ℕ) : ℝ) * B ^ k := by + have hsum : + ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k + ≤ ((n - 1 : ℕ) : ℝ) * B ^ k := by + calc + ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k + ≤ ∑ _t ∈ (Finset.univ.erase (0 : ZMod n)), B ^ k := by + apply Finset.sum_le_sum + intro t ht + exact pow_le_pow_left₀ (norm_nonneg _) (hB t (Finset.ne_of_mem_erase ht)) k + _ = ((n - 1 : ℕ) : ℝ) * B ^ k := by simp + calc + ‖shuniaScaledCoeff a n k α i - shuniaMainTerm n k α‖ + ≤ ‖(n : ℂ)⁻¹‖ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k := + norm_shuniaScaledCoeff_sub_mainTerm_le_sum a n k α hα i + _ ≤ ‖(n : ℂ)⁻¹‖ * (((n - 1 : ℕ) : ℝ) * B ^ k) := + mul_le_mul_of_nonneg_left hsum (norm_nonneg _) + _ = ‖(n : ℂ)⁻¹‖ * ((n - 1 : ℕ) : ℝ) * B ^ k := by ring + +private lemma norm_one_sub_stdAddChar (n : ℕ) [NeZero n] (t : ZMod n) : + ‖(1 : ℂ) - ZMod.stdAddChar t‖ = + ‖2 * Real.sin (Real.pi * (t.val : ℝ) / n)‖ := by + rw [ZMod.stdAddChar_apply, ZMod.toCircle_eq_circleExp] + change ‖(1 : ℂ) - Complex.exp ((2 * Real.pi * ((t.val : ℝ) / n) : ℝ) * Complex.I)‖ = + ‖2 * Real.sin (Real.pi * (t.val : ℝ) / n)‖ + rw [← norm_neg, neg_sub] + rw [show ((2 * Real.pi * ((t.val : ℝ) / n) : ℝ) : ℂ) * Complex.I = + Complex.I * ((2 * Real.pi * (t.val : ℝ) / n : ℝ) : ℂ) by + rw [mul_comm] + norm_cast + ring_nf] + rw [Complex.norm_exp_I_mul_ofReal_sub_one] + congr 2 + ring_nf + +private lemma four_div_le_two_mul_sin_pi_mul_div_of_le_half + (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (hmhalf : m ≤ n / 2) : + (4 : ℝ) / n ≤ 2 * Real.sin (Real.pi * (m : ℝ) / n) := by + have hnR : (0 : ℝ) < n := by exact_mod_cast hn + have hmR : (1 : ℝ) ≤ m := by exact_mod_cast hm + have htwom : 2 * m ≤ n := by omega + have htwomR : (2 : ℝ) * m ≤ n := by exact_mod_cast htwom + have hx0 : (0 : ℝ) ≤ Real.pi * (m : ℝ) / n := by positivity + have hxhalf : Real.pi * (m : ℝ) / n ≤ Real.pi / 2 := by + rw [div_le_iff₀ hnR] + nlinarith [Real.pi_pos] + have hsin := Real.mul_le_sin hx0 hxhalf + have hscale : + (2 : ℝ) * m / n = 2 / Real.pi * (Real.pi * (m : ℝ) / n) := by + field_simp + have hone : (2 : ℝ) / n ≤ 2 * m / n := by + apply (div_le_div_iff_of_pos_right hnR).2 + linarith + have : (2 : ℝ) / n ≤ Real.sin (Real.pi * (m : ℝ) / n) := by + calc + (2 : ℝ) / n ≤ 2 * m / n := hone + _ = 2 / Real.pi * (Real.pi * (m : ℝ) / n) := hscale + _ ≤ Real.sin (Real.pi * (m : ℝ) / n) := hsin + calc + (4 : ℝ) / n = 2 * (2 / n) := by ring + _ ≤ 2 * Real.sin (Real.pi * (m : ℝ) / n) := + mul_le_mul_of_nonneg_left this (by norm_num) + +private lemma four_div_le_norm_one_sub_stdAddChar + (n : ℕ) [NeZero n] (t : ZMod n) (ht : t ≠ 0) : + (4 : ℝ) / n ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ := by + have hn : 0 < n := NeZero.pos n + have hm : 0 < t.val := ZMod.val_pos.mpr ht + have hmn : t.val < n := t.val_lt + rw [norm_one_sub_stdAddChar] + have hsin_nonneg : + 0 ≤ Real.sin (Real.pi * (t.val : ℝ) / n) := by + apply Real.sin_nonneg_of_nonneg_of_le_pi + · positivity + · have hnR : (0 : ℝ) < n := by exact_mod_cast hn + rw [div_le_iff₀ hnR] + have hmnR : (t.val : ℝ) ≤ n := by exact_mod_cast hmn.le + nlinarith [Real.pi_pos] + rw [Real.norm_of_nonneg (mul_nonneg (by norm_num) hsin_nonneg)] + by_cases hhalf : t.val ≤ n / 2 + · exact four_div_le_two_mul_sin_pi_mul_div_of_le_half n t.val hn hm hhalf + · let d := n - t.val + have hd : 0 < d := Nat.sub_pos_of_lt hmn + have hdhalf : d ≤ n / 2 := by + dsimp [d] + omega + have hsin : + Real.sin (Real.pi * (t.val : ℝ) / n) = + Real.sin (Real.pi * (d : ℝ) / n) := by + calc + Real.sin (Real.pi * (t.val : ℝ) / n) = + Real.sin (Real.pi - Real.pi * (t.val : ℝ) / n) := + (Real.sin_pi_sub _).symm + _ = Real.sin (Real.pi * (d : ℝ) / n) := by + congr 1 + dsimp [d] + have hnR : (n : ℝ) ≠ 0 := by positivity + rw [Nat.cast_sub hmn.le] + field_simp + rw [hsin] + exact four_div_le_two_mul_sin_pi_mul_div_of_le_half n d hn hd hdhalf + +private lemma norm_one_add_mul_stdAddChar_sq + (n : ℕ) [NeZero n] (α : ℝ) (t : ZMod n) : + ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ 2 = + (1 + α) ^ 2 - α * ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := by + rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq] + simp [Complex.normSq_add, Complex.normSq_sub, Complex.normSq_mul, + Complex.normSq_ofReal] + rw [show Complex.normSq (ZMod.stdAddChar t) = 1 by + rw [Complex.normSq_eq_norm_sq] + simp] + ring + +private lemma norm_one_add_mul_stdAddChar_le_sqrt + (n : ℕ) [NeZero n] (α : ℝ) (hα : 0 ≤ α) (t : ZMod n) (ht : t ≠ 0) : + ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ≤ + Real.sqrt ((1 + α) ^ 2 - 16 * α / n ^ 2) := by + have hchord := four_div_le_norm_one_sub_stdAddChar n t ht + have hchord_sq : + (16 : ℝ) / n ^ 2 ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := by + have hsquare := pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ 4 / n) hchord 2 + calc + (16 : ℝ) / n ^ 2 = ((4 : ℝ) / n) ^ 2 := by ring + _ ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := hsquare + apply Real.le_sqrt_of_sq_le + rw [norm_one_add_mul_stdAddChar_sq] + calc + (1 + α) ^ 2 - α * ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 + ≤ (1 + α) ^ 2 - α * ((16 : ℝ) / n ^ 2) := + sub_le_sub_left (mul_le_mul_of_nonneg_left hchord_sq hα) _ + _ = (1 + α) ^ 2 - 16 * α / n ^ 2 := by ring + +/-- A uniform squared spectral ratio for all nontrivial Fourier modes. -/ +private noncomputable def shuniaQSq (n : ℕ) (α : ℝ) : ℝ := + 1 - 16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2) + +private lemma shuniaQSq_nonneg + (n : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) : + 0 ≤ shuniaQSq n α := by + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn + have hnsq : (4 : ℝ) ≤ (n : ℝ) ^ 2 := by nlinarith + have hαsq : 4 * α ≤ (1 + α) ^ 2 := by nlinarith [sq_nonneg (α - 1)] + have hden : (0 : ℝ) < (n : ℝ) ^ 2 * (1 + α) ^ 2 := by positivity + rw [shuniaQSq, sub_nonneg, div_le_one hden] + have hmul := mul_le_mul hnsq hαsq (mul_nonneg (by norm_num) hα) (by norm_num) + nlinarith + +private lemma shuniaQSq_le_exp (n : ℕ) (α : ℝ) : + shuniaQSq n α ≤ + Real.exp (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2))) := by + simpa [shuniaQSq, add_comm] using + Real.add_one_le_exp (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2))) + +/-- The exponent appearing in the uniform decay estimate. -/ +private noncomputable def shuniaDecay (a n : ℕ) (α : ℝ) : ℝ := + 16 * a * α / (n * (1 + α) ^ 2) + +private lemma shuniaQSq_pow_le_exp_neg_decay + (a n : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) : + shuniaQSq n α ^ (a * n) ≤ Real.exp (-shuniaDecay a n α) := by + have hpow := pow_le_pow_left₀ (shuniaQSq_nonneg n hn α hα) + (shuniaQSq_le_exp n α) (a * n) + calc + shuniaQSq n α ^ (a * n) + ≤ Real.exp (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2))) ^ (a * n) := hpow + _ = Real.exp ((a * n : ℕ) * + (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2)))) := by + rw [Real.exp_nat_mul] + _ = Real.exp (-shuniaDecay a n α) := by + congr 1 + rw [shuniaDecay] + have hn0 : (n : ℝ) ≠ 0 := by + exact_mod_cast (show n ≠ 0 by omega) + push_cast + field_simp + +private lemma five_thirds_pow_le_two_pow_sub_one (n : ℕ) (hn : 6 ≤ n) : + ((5 : ℝ) / 3) ^ n ≤ 2 ^ (n - 1) := by + induction n, hn using Nat.le_induction with + | base => norm_num + | succ n hn ih => + rw [pow_succ] + calc + ((5 : ℝ) / 3) ^ n * (5 / 3) ≤ 2 ^ (n - 1) * (5 / 3) := + mul_le_mul_of_nonneg_right ih (by norm_num) + _ ≤ 2 ^ (n - 1) * 2 := + mul_le_mul_of_nonneg_left (by norm_num) (by positivity) + _ = 2 ^ (n + 1 - 1) := by + rw [show n + 1 - 1 = (n - 1) + 1 by omega, pow_succ] + +private lemma five_thirds_le_of_root_and_log_bound + (a n : ℕ) (hn : 6 ≤ n) (α : ℝ) (hα : 0 ≤ α) + (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : + (5 : ℝ) / 3 ≤ α := by + have hpow : ((5 : ℝ) / 3) ^ n ≤ α ^ n := by + calc + ((5 : ℝ) / 3) ^ n ≤ 2 ^ (n - 1) := five_thirds_pow_le_two_pow_sub_one n hn + _ ≤ (a : ℝ) := by exact_mod_cast ha + _ = α ^ n := hroot.symm + by_contra h + have hlt : α < (5 : ℝ) / 3 := lt_of_not_ge h + have hstrict : α ^ n < ((5 : ℝ) / 3) ^ n := + pow_lt_pow_left₀ hlt hα (by omega) + exact (not_lt_of_ge hpow hstrict) + +private lemma decay_lower_bound_of_six_le + (a n : ℕ) (hn : 6 ≤ n) (α : ℝ) (hα : 0 ≤ α) + (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : + (25 : ℝ) / 4 * a / (n * α) ≤ shuniaDecay a n α := by + have hα53 := five_thirds_le_of_root_and_log_bound a n hn α hα hroot ha + have hnR : (0 : ℝ) < n := by positivity + have hαpos : 0 < α := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 5 / 3) hα53 + have hlinear : 1 + α ≤ (8 / 5 : ℝ) * α := by linarith + have hsquare : (1 + α) ^ 2 ≤ ((8 / 5 : ℝ) * α) ^ 2 := + pow_le_pow_left₀ (by positivity) hlinear 2 + rw [shuniaDecay] + have hnum : (0 : ℝ) ≤ 16 * a * α := by positivity + calc + (25 : ℝ) / 4 * a / (n * α) = + 16 * a * α / (n * (((8 / 5 : ℝ) * α) ^ 2)) := by + field_simp + ring + _ ≤ 16 * a * α / (n * (1 + α) ^ 2) := by + apply div_le_div_of_nonneg_left hnum + · positivity + · exact mul_le_mul_of_nonneg_left hsquare (by positivity) + +private lemma ten_factorial_poly_lt_two_pow (n : ℕ) (hn : 10 ≤ n) : + 16 * 10 ! * 4 ^ 10 * n ^ 12 < 25 ^ 10 * 2 ^ (7 * (n - 1)) := by + induction n, hn using Nat.le_induction with + | base => norm_num [Nat.factorial] + | succ n hn ih => + have hlinear : 10 * (n + 1) ≤ 11 * n := by omega + have hpow := Nat.pow_le_pow_left hlinear 12 + have hconstant : 11 ^ 12 < 128 * 10 ^ 12 := by norm_num + have hnpos : 0 < n ^ 12 := Nat.pow_pos (by omega) + have hpoly : (n + 1) ^ 12 < 128 * n ^ 12 := by + have hscaled : + 10 ^ 12 * (n + 1) ^ 12 < 10 ^ 12 * (128 * n ^ 12) := by + calc + 10 ^ 12 * (n + 1) ^ 12 = (10 * (n + 1)) ^ 12 := by rw [mul_pow] + _ ≤ (11 * n) ^ 12 := hpow + _ = 11 ^ 12 * n ^ 12 := by rw [mul_pow] + _ < (128 * 10 ^ 12) * n ^ 12 := + Nat.mul_lt_mul_of_pos_right hconstant hnpos + _ = 10 ^ 12 * (128 * n ^ 12) := by ring + omega + let C : ℕ := 16 * 10 ! * 4 ^ 10 + let R : ℕ := 25 ^ 10 * 2 ^ (7 * (n - 1)) + have hC : 0 < C := by + dsimp [C] + positivity + have hstep₁ : C * (n + 1) ^ 12 < 128 * (C * n ^ 12) := by + calc + C * (n + 1) ^ 12 < C * (128 * n ^ 12) := + Nat.mul_lt_mul_of_pos_left hpoly hC + _ = 128 * (C * n ^ 12) := by ring + have hstep₂ : 128 * (C * n ^ 12) < 128 * R := by + apply Nat.mul_lt_mul_of_pos_left + · simpa [C, R] using ih + · norm_num + calc + 16 * 10 ! * 4 ^ 10 * (n + 1) ^ 12 = C * (n + 1) ^ 12 := by rfl + _ < 128 * (C * n ^ 12) := hstep₁ + _ < 128 * R := hstep₂ + _ = 25 ^ 10 * 2 ^ (7 * (n + 1 - 1)) := by + dsimp [R] + rw [show 7 * n = 7 * (n - 1) + 7 by omega, pow_add] + norm_num + ring + +private lemma decay_large_of_ten_le + (a n : ℕ) (hn : 10 ≤ n) (α : ℝ) (hα : 0 ≤ α) + (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : + (16 : ℝ) * n * (n - 1) * a ^ 2 < Real.exp (shuniaDecay a n α) := by + have hn6 : 6 ≤ n := hn.trans' (by norm_num) + have hα53 := five_thirds_le_of_root_and_log_bound a n hn6 α hα hroot ha + have hα1 : (1 : ℝ) ≤ α := le_trans (by norm_num) hα53 + have hαpos : 0 < α := zero_lt_one.trans_le hα1 + have haPos : (0 : ℝ) < a := by + exact_mod_cast (lt_of_lt_of_le (Nat.pow_pos (by decide)) ha) + have hα10 : α ^ 10 ≤ (a : ℝ) := by + calc + α ^ 10 ≤ α ^ n := pow_le_pow_right₀ hα1 hn + _ = (a : ℝ) := hroot + have ha7 : 2 ^ (7 * (n - 1)) ≤ a ^ 7 := by + calc + 2 ^ (7 * (n - 1)) = (2 ^ (n - 1)) ^ 7 := by + rw [show 7 * (n - 1) = (n - 1) * 7 by omega, pow_mul] + _ ≤ a ^ 7 := Nat.pow_le_pow_left ha 7 + have hpolyNat : + 16 * 10 ! * 4 ^ 10 * n ^ 12 < 25 ^ 10 * a ^ 7 := + (ten_factorial_poly_lt_two_pow n hn).trans_le + (Nat.mul_le_mul_left (25 ^ 10) ha7) + have hpoly : + (16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 12 < + (25 : ℝ) ^ 10 * (a : ℝ) ^ 7 := by + exact_mod_cast hpolyNat + have hcross : + ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * α ^ 10) < + (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by + calc + ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * α ^ 10) + ≤ ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 12) * (a : ℝ) ^ 3 := by + have haR : (0 : ℝ) ≤ a := by positivity + calc + ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * α ^ 10) + ≤ ((16 : ℝ) * n * n * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * α ^ 10) := by + gcongr + linarith + _ ≤ ((16 : ℝ) * n * n * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * (a : ℝ)) := by gcongr + _ = ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 12) * (a : ℝ) ^ 3 := by + ring + _ < ((25 : ℝ) ^ 10 * (a : ℝ) ^ 7) * (a : ℝ) ^ 3 := + mul_lt_mul_of_pos_right hpoly (pow_pos haPos 3) + _ = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by ring + let L : ℝ := (25 : ℝ) / 4 * a / (n * α) + have hL0 : 0 ≤ L := by + dsimp [L] + positivity + have hLpow : + L ^ 10 = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 / (4 ^ 10 * n ^ 10 * α ^ 10) := by + dsimp [L] + field_simp + have hterm : + (16 : ℝ) * n * (n - 1) * a ^ 2 < L ^ 10 / (10 ! : ℕ) := by + rw [hLpow] + apply (lt_div_iff₀ (by positivity : (0 : ℝ) < (10 ! : ℕ))).2 + apply (lt_div_iff₀ (by positivity : (0 : ℝ) < 4 ^ 10 * n ^ 10 * α ^ 10)).2 + exact hcross + have hLdecay : L ≤ shuniaDecay a n α := + decay_lower_bound_of_six_le a n hn6 α hα hroot ha + have hdecay0 : 0 ≤ shuniaDecay a n α := hL0.trans hLdecay + calc + (16 : ℝ) * n * (n - 1) * a ^ 2 + < L ^ 10 / (10 ! : ℕ) := hterm + _ ≤ shuniaDecay a n α ^ 10 / (10 ! : ℕ) := by + gcongr + _ ≤ Real.exp (shuniaDecay a n α) := + Real.pow_div_factorial_le_exp (x := shuniaDecay a n α) hdecay0 10 + +private lemma small_n_decay_numeric (n : ℕ) (hn6 : 6 ≤ n) (hn10 : n < 10) : + (16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1) < + 25 ^ 10 * (((2 ^ (n - 1) : ℕ) : ℝ) ^ 6) * + ((5 : ℝ) / 3) ^ (2 * n - 10) := by + interval_cases n <;> norm_num [Nat.factorial] + +private lemma decay_large_of_six_le_of_lt_ten + (a n : ℕ) (hn6 : 6 ≤ n) (hn10 : n < 10) (α : ℝ) (hα : 0 ≤ α) + (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : + (16 : ℝ) * n * (n - 1) * a ^ 2 < Real.exp (shuniaDecay a n α) := by + have hα53 := five_thirds_le_of_root_and_log_bound a n hn6 α hα hroot ha + have hαpos : 0 < α := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 5 / 3) hα53 + have haPos : (0 : ℝ) < a := by + exact_mod_cast (lt_of_lt_of_le (Nat.pow_pos (by decide)) ha) + have ha6 : ((2 ^ (n - 1) : ℕ) : ℝ) ^ 6 ≤ (a : ℝ) ^ 6 := by + exact_mod_cast Nat.pow_le_pow_left ha 6 + have hαrem : + ((5 : ℝ) / 3) ^ (2 * n - 10) ≤ α ^ (2 * n - 10) := + pow_le_pow_left₀ (by norm_num) hα53 _ + have hidentity : + (a : ℝ) ^ 6 * α ^ (2 * n - 10) * α ^ 10 = (a : ℝ) ^ 8 := by + rw [← hroot] + simp only [← pow_mul] + rw [← pow_add, ← pow_add] + congr 1 + omega + have hratio : + ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1)) * α ^ 10 < + 25 ^ 10 * (a : ℝ) ^ 8 := by + calc + ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1)) * α ^ 10 + < (25 ^ 10 * ((2 ^ (n - 1) : ℕ) : ℝ) ^ 6 * + ((5 : ℝ) / 3) ^ (2 * n - 10)) * α ^ 10 := + mul_lt_mul_of_pos_right (small_n_decay_numeric n hn6 hn10) + (pow_pos hαpos 10) + _ ≤ (25 ^ 10 * (a : ℝ) ^ 6 * α ^ (2 * n - 10)) * α ^ 10 := by + gcongr + _ = 25 ^ 10 * (a : ℝ) ^ 8 := by rw [← hidentity]; ring + have hcross : + ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * α ^ 10) < + (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by + calc + ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * + (4 ^ 10 * n ^ 10 * α ^ 10) + = (((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1)) * + α ^ 10) * (a : ℝ) ^ 2 := by ring + _ < (25 ^ 10 * (a : ℝ) ^ 8) * (a : ℝ) ^ 2 := + mul_lt_mul_of_pos_right hratio (pow_pos haPos 2) + _ = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by ring + let L : ℝ := (25 : ℝ) / 4 * a / (n * α) + have hL0 : 0 ≤ L := by + dsimp [L] + positivity + have hLpow : + L ^ 10 = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 / (4 ^ 10 * n ^ 10 * α ^ 10) := by + dsimp [L] + field_simp + have hterm : + (16 : ℝ) * n * (n - 1) * a ^ 2 < L ^ 10 / (10 ! : ℕ) := by + rw [hLpow] + apply (lt_div_iff₀ (by positivity : (0 : ℝ) < (10 ! : ℕ))).2 + apply (lt_div_iff₀ (by positivity : (0 : ℝ) < 4 ^ 10 * n ^ 10 * α ^ 10)).2 + exact hcross + have hLdecay : L ≤ shuniaDecay a n α := + decay_lower_bound_of_six_le a n hn6 α hα hroot ha + have hdecay0 : 0 ≤ shuniaDecay a n α := hL0.trans hLdecay + calc + (16 : ℝ) * n * (n - 1) * a ^ 2 + < L ^ 10 / (10 ! : ℕ) := hterm + _ ≤ shuniaDecay a n α ^ 10 / (10 ! : ℕ) := by gcongr + _ ≤ Real.exp (shuniaDecay a n α) := + Real.pow_div_factorial_le_exp (x := shuniaDecay a n α) hdecay0 10 + +private lemma norm_one_add_mul_stdAddChar_sq_le + (n : ℕ) [NeZero n] (α : ℝ) (hα : 0 ≤ α) (t : ZMod n) (ht : t ≠ 0) : + ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ 2 ≤ + (1 + α) ^ 2 * shuniaQSq n α := by + have hchord := four_div_le_norm_one_sub_stdAddChar n t ht + have hchord_sq : + (16 : ℝ) / n ^ 2 ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := by + have hsquare := pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ 4 / n) hchord 2 + calc + (16 : ℝ) / n ^ 2 = ((4 : ℝ) / n) ^ 2 := by ring + _ ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := hsquare + rw [norm_one_add_mul_stdAddChar_sq] + calc + (1 + α) ^ 2 - α * ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 + ≤ (1 + α) ^ 2 - α * ((16 : ℝ) / n ^ 2) := + sub_le_sub_left (mul_le_mul_of_nonneg_left hchord_sq hα) _ + _ = (1 + α) ^ 2 * shuniaQSq n α := by + rw [shuniaQSq] + have hn : (n : ℝ) ≠ 0 := by exact_mod_cast (NeZero.ne n) + have hα1 : (1 + α : ℝ) ≠ 0 := by positivity + field_simp + +private lemma norm_one_add_mul_stdAddChar_even_pow_le + (a n : ℕ) [NeZero n] (α : ℝ) (hα : 0 ≤ α) (t : ZMod n) (ht : t ≠ 0) : + ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ (2 * a * n) ≤ + (1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n) := by + have hsquare := norm_one_add_mul_stdAddChar_sq_le n α hα t ht + have hpow := pow_le_pow_left₀ (sq_nonneg ‖1 + (α : ℂ) * ZMod.stdAddChar t‖) + hsquare (a * n) + calc + ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ (2 * a * n) = + (‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ 2) ^ (a * n) := by + simpa [mul_assoc] using + (pow_mul ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ 2 (a * n)) + _ ≤ ((1 + α) ^ 2 * shuniaQSq n α) ^ (a * n) := hpow + _ = (1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n) := by + rw [mul_pow] + congr 1 + simpa [mul_assoc] using (pow_mul (1 + α) 2 (a * n)).symm + +/-- The relative Fourier-error factor at the exponent `2 * a * n`. -/ +private noncomputable def shuniaError (a n : ℕ) (α : ℝ) : ℝ := + ((n - 1 : ℕ) : ℝ) * shuniaQSq n α ^ (a * n) + +private lemma norm_shuniaScaledCoeff_sub_mainTerm_at_K_le + (a n : ℕ) [NeZero n] (α : ℝ) (hroot : α ^ n = a) (hα : 0 ≤ α) + (i : ZMod n) : + ‖shuniaScaledCoeff a n (2 * a * n) α i - shuniaMainTerm n (2 * a * n) α‖ ≤ + ‖(n : ℂ)⁻¹‖ * (1 + α) ^ (2 * a * n) * shuniaError a n α := by + refine (norm_shuniaScaledCoeff_sub_mainTerm_le_sum + a n (2 * a * n) α hroot i).trans ?_ + have hsum : + ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ (2 * a * n) ≤ + ((n - 1 : ℕ) : ℝ) * + ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n)) := by + calc + ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ (2 * a * n) + ≤ ∑ _t ∈ (Finset.univ.erase (0 : ZMod n)), + ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n)) := by + apply Finset.sum_le_sum + intro t ht + exact norm_one_add_mul_stdAddChar_even_pow_le a n α hα (-t) + (neg_ne_zero.mpr (Finset.ne_of_mem_erase ht)) + _ = ((n - 1 : ℕ) : ℝ) * + ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n)) := by simp + calc + ‖(n : ℂ)⁻¹‖ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), + ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ (2 * a * n) + ≤ ‖(n : ℂ)⁻¹‖ * (((n - 1 : ℕ) : ℝ) * + ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n))) := + mul_le_mul_of_nonneg_left hsum (norm_nonneg _) + _ = ‖(n : ℂ)⁻¹‖ * (1 + α) ^ (2 * a * n) * shuniaError a n α := by + rw [shuniaError] + ring + +end Nat From bd06b88abaebdc9fac7e63f82844afb13522e27b Mon Sep 17 00:00:00 2001 From: rbajaj5 Date: Fri, 24 Jul 2026 00:43:02 -0400 Subject: [PATCH 2/3] Complete Shunia integer-root formalization Co-authored-by: Ben Burns --- Mathlib.lean | 2 + Mathlib/NumberTheory/Shunia.lean | 684 --------- Mathlib/NumberTheory/ShuniaIntegerRoot.lean | 1219 +++++++++++++++++ .../ShuniaIntegerRoot/Estimates.lean | 543 ++++++++ 4 files changed, 1764 insertions(+), 684 deletions(-) delete mode 100644 Mathlib/NumberTheory/Shunia.lean create mode 100644 Mathlib/NumberTheory/ShuniaIntegerRoot.lean create mode 100644 Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean diff --git a/Mathlib.lean b/Mathlib.lean index 638124f2103e51..1c3d8d2c01f28a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5936,6 +5936,8 @@ public import Mathlib.NumberTheory.Rayleigh public import Mathlib.NumberTheory.Real.GoldenRatio public import Mathlib.NumberTheory.Real.Irrational public import Mathlib.NumberTheory.SelbergSieve +public import Mathlib.NumberTheory.ShuniaIntegerRoot +public import Mathlib.NumberTheory.ShuniaIntegerRoot.Estimates public import Mathlib.NumberTheory.SiegelsLemma public import Mathlib.NumberTheory.SmoothNumbers public import Mathlib.NumberTheory.SumFourSquares diff --git a/Mathlib/NumberTheory/Shunia.lean b/Mathlib/NumberTheory/Shunia.lean deleted file mode 100644 index e5b5f2e1df19dc..00000000000000 --- a/Mathlib/NumberTheory/Shunia.lean +++ /dev/null @@ -1,684 +0,0 @@ -/- -Copyright (c) 2026 rbajaj5. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: rbajaj5 --/ -module - -public import Mathlib.Analysis.Fourier.ZMod -public import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas -public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds -public import Mathlib.Algebra.BigOperators.ModEq -public import Mathlib.Data.Nat.Log -public import Mathlib.Tactic - -/-! -# Shunia's integer-root formula - -This file develops the coefficient and Fourier estimates needed to formalize Conjecture 6.1 -from Joseph M. Shunia, -*Polynomial quotient rings and Kronecker substitution for deriving combinatorial identities*. - -The intended public statement will be phrased using `Nat.nthRoot`: the quotient of the two least -nonnegative residues is one more than the integer `n`-th root. --/ - -public section - -namespace Nat - -open scoped BigOperators - -/-- The base used for the Kronecker substitution in Shunia's formula. -/ -def shuniaBase (a n : ℕ) : ℕ := a ^ (2 * a * n) - -/-- The modulus used in Shunia's formula. -/ -def shuniaModulus (a n : ℕ) : ℕ := shuniaBase a n ^ n - a - -/-- The denominator residue in Shunia's formula. -/ -def shuniaDenominator (a n : ℕ) : ℕ := - (shuniaBase a n + 1) ^ (2 * a * n) % shuniaModulus a n - -/-- The numerator residue in Shunia's formula. -/ -def shuniaNumerator (a n : ℕ) : ℕ := - (shuniaBase a n + 1) ^ (2 * a * n + 1) % shuniaModulus a n - -/-- The coefficient of residue class `i` in the reduction of `(1 + T) ^ k` modulo `T ^ n - a`. -/ -def shuniaCoeff (a n k : ℕ) (i : ZMod n) : ℕ := - ∑ j ∈ Finset.range (k + 1), - if (j : ZMod n) = i then k.choose j * a ^ (j / n) else 0 - -/-- Evaluation at `X` of the reduced coefficient vector for `(1 + T) ^ k`. -/ -def shuniaCoeffEval (a n k X : ℕ) [NeZero n] : ℕ := - ∑ i : ZMod n, shuniaCoeff a n k i * X ^ i.val - -private lemma shuniaCoeffEval_eq_sum (a n k X : ℕ) [NeZero n] : - shuniaCoeffEval a n k X = - ∑ j ∈ Finset.range (k + 1), k.choose j * a ^ (j / n) * X ^ (j % n) := by - classical - simp only [shuniaCoeffEval, shuniaCoeff, Finset.sum_mul] - rw [Finset.sum_comm] - apply Finset.sum_congr rfl - intro j hj - simp [eq_comm, ZMod.val_natCast] - -private lemma pow_modEq_div_mod (a n X j : ℕ) (haX : a ≤ X ^ n) : - X ^ j ≡ a ^ (j / n) * X ^ (j % n) [MOD X ^ n - a] := by - have hbase : X ^ n ≡ a [MOD X ^ n - a] := - ((Nat.modEq_iff_dvd' haX).2 dvd_rfl).symm - calc - X ^ j = X ^ (n * (j / n) + j % n) := by - congr 1 - simpa [mul_comm] using (Nat.div_add_mod' j n).symm - _ = (X ^ n) ^ (j / n) * X ^ (j % n) := by rw [pow_add, pow_mul] - _ ≡ a ^ (j / n) * X ^ (j % n) [MOD X ^ n - a] := - (hbase.pow (j / n)).mul_right _ - -private lemma pow_add_one_modEq_coeffEval (a n k X : ℕ) [NeZero n] (haX : a ≤ X ^ n) : - (X + 1) ^ k ≡ shuniaCoeffEval a n k X [MOD X ^ n - a] := by - rw [shuniaCoeffEval_eq_sum] - have hsum := Nat.ModEq.sum (s := Finset.range (k + 1)) fun j _ ↦ - (pow_modEq_div_mod a n X j haX).mul_left (k.choose j) - simpa [add_pow, mul_assoc, mul_comm, mul_left_comm] using hsum - -private noncomputable def shuniaScaledCoeff (a n k : ℕ) (α : ℝ) (i : ZMod n) : ℂ := - shuniaCoeff a n k i * (α : ℂ) ^ i.val - -private lemma cast_pow_div_mul_pow_mod {a n j : ℕ} {α : ℝ} (hα : α ^ n = a) : - ((a ^ (j / n) : ℕ) : ℂ) * (α : ℂ) ^ (j % n) = (α : ℂ) ^ j := by - have hαc : (α : ℂ) ^ n = (a : ℂ) := by exact_mod_cast hα - rw [Nat.cast_pow, ← hαc, ← pow_mul, ← pow_add] - congr 1 - simpa [mul_comm] using Nat.div_add_mod' j n - -private lemma stdAddChar_neg_natCast_mul (n j : ℕ) [NeZero n] (t : ZMod n) : - ZMod.stdAddChar (-((j : ZMod n) * t)) = ZMod.stdAddChar (-t) ^ j := by - rw [show -((j : ZMod n) * t) = j • (-t) by simp [nsmul_eq_mul]] - exact AddChar.map_nsmul_eq_pow (ZMod.stdAddChar (N := n)) j (-t) - -private lemma dft_shuniaScaledCoeff (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) - (t : ZMod n) : - ZMod.dft (shuniaScaledCoeff a n k α) t = - (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by - classical - rw [ZMod.dft_apply] - simp only [shuniaScaledCoeff, shuniaCoeff, smul_eq_mul, Nat.cast_sum, Nat.cast_ite, - Nat.cast_mul, Nat.cast_pow, Nat.cast_zero] - conv_lhs => - enter [2, i] - rw [← mul_assoc, Finset.mul_sum, Finset.sum_mul] - rw [Finset.sum_comm] - calc - _ = ∑ j ∈ Finset.range (k + 1), - (k.choose j : ℂ) * ((α : ℂ) * ZMod.stdAddChar (-t)) ^ j := by - apply Finset.sum_congr rfl - intro j hj - simp only [mul_ite, ite_mul, mul_zero, zero_mul, eq_comm, Fintype.sum_ite_eq'] - rw [ZMod.val_natCast, stdAddChar_neg_natCast_mul] - have hpower : - (a : ℂ) ^ (j / n) * (α : ℂ) ^ (j % n) = (α : ℂ) ^ j := by - simpa only [Nat.cast_pow] using - (cast_pow_div_mul_pow_mod (a := a) (n := n) (j := j) hα) - rw [show ZMod.stdAddChar (-t) ^ j * - ((k.choose j : ℂ) * (a : ℂ) ^ (j / n)) * (α : ℂ) ^ (j % n) = - (k.choose j : ℂ) * ZMod.stdAddChar (-t) ^ j * - ((a : ℂ) ^ (j / n) * (α : ℂ) ^ (j % n)) by ring, - hpower, mul_pow] - ring - _ = (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by - simpa [mul_comm, add_comm] using - (add_pow ((α : ℂ) * ZMod.stdAddChar (-t)) 1 k).symm - -private lemma shuniaScaledCoeff_eq_fourierSum - (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) : - shuniaScaledCoeff a n k α i = - (n : ℂ)⁻¹ * ∑ t : ZMod n, - ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by - have hinv := - congrFun ((ZMod.dft (N := n) (E := ℂ)).symm_apply_apply - (shuniaScaledCoeff a n k α)) i - rw [ZMod.invDFT_apply] at hinv - simpa only [smul_eq_mul, dft_shuniaScaledCoeff a n k α hα] using hinv.symm - -/-- The positive real contribution of the trivial character in the Fourier formula. -/ -private noncomputable def shuniaMainTerm (n k : ℕ) (α : ℝ) : ℂ := - (n : ℂ)⁻¹ * (1 + (α : ℂ)) ^ k - -private lemma shuniaScaledCoeff_sub_mainTerm - (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) : - shuniaScaledCoeff a n k α i - shuniaMainTerm n k α = - (n : ℂ)⁻¹ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k := by - rw [shuniaScaledCoeff_eq_fourierSum a n k α hα, shuniaMainTerm] - rw [← Finset.add_sum_erase Finset.univ - (fun t : ZMod n ↦ - ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k) - (Finset.mem_univ (0 : ZMod n))] - simp - ring - -private lemma norm_shuniaScaledCoeff_sub_mainTerm_le_sum - (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) : - ‖shuniaScaledCoeff a n k α i - shuniaMainTerm n k α‖ ≤ - ‖(n : ℂ)⁻¹‖ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k := by - rw [shuniaScaledCoeff_sub_mainTerm a n k α hα, norm_mul] - gcongr - calc - ‖∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ZMod.stdAddChar (t * i) * (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k‖ - ≤ ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖ZMod.stdAddChar (t * i) * - (1 + (α : ℂ) * ZMod.stdAddChar (-t)) ^ k‖ := norm_sum_le _ _ - _ = ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k := by - apply Finset.sum_congr rfl - intro t ht - simp [norm_pow] - -private lemma norm_shuniaScaledCoeff_sub_mainTerm_le - (a n k : ℕ) [NeZero n] (α : ℝ) (hα : α ^ n = a) (i : ZMod n) (B : ℝ) - (hB : ∀ t : ZMod n, t ≠ 0 → ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ≤ B) : - ‖shuniaScaledCoeff a n k α i - shuniaMainTerm n k α‖ ≤ - ‖(n : ℂ)⁻¹‖ * ((n - 1 : ℕ) : ℝ) * B ^ k := by - have hsum : - ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k - ≤ ((n - 1 : ℕ) : ℝ) * B ^ k := by - calc - ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k - ≤ ∑ _t ∈ (Finset.univ.erase (0 : ZMod n)), B ^ k := by - apply Finset.sum_le_sum - intro t ht - exact pow_le_pow_left₀ (norm_nonneg _) (hB t (Finset.ne_of_mem_erase ht)) k - _ = ((n - 1 : ℕ) : ℝ) * B ^ k := by simp - calc - ‖shuniaScaledCoeff a n k α i - shuniaMainTerm n k α‖ - ≤ ‖(n : ℂ)⁻¹‖ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ k := - norm_shuniaScaledCoeff_sub_mainTerm_le_sum a n k α hα i - _ ≤ ‖(n : ℂ)⁻¹‖ * (((n - 1 : ℕ) : ℝ) * B ^ k) := - mul_le_mul_of_nonneg_left hsum (norm_nonneg _) - _ = ‖(n : ℂ)⁻¹‖ * ((n - 1 : ℕ) : ℝ) * B ^ k := by ring - -private lemma norm_one_sub_stdAddChar (n : ℕ) [NeZero n] (t : ZMod n) : - ‖(1 : ℂ) - ZMod.stdAddChar t‖ = - ‖2 * Real.sin (Real.pi * (t.val : ℝ) / n)‖ := by - rw [ZMod.stdAddChar_apply, ZMod.toCircle_eq_circleExp] - change ‖(1 : ℂ) - Complex.exp ((2 * Real.pi * ((t.val : ℝ) / n) : ℝ) * Complex.I)‖ = - ‖2 * Real.sin (Real.pi * (t.val : ℝ) / n)‖ - rw [← norm_neg, neg_sub] - rw [show ((2 * Real.pi * ((t.val : ℝ) / n) : ℝ) : ℂ) * Complex.I = - Complex.I * ((2 * Real.pi * (t.val : ℝ) / n : ℝ) : ℂ) by - rw [mul_comm] - norm_cast - ring_nf] - rw [Complex.norm_exp_I_mul_ofReal_sub_one] - congr 2 - ring_nf - -private lemma four_div_le_two_mul_sin_pi_mul_div_of_le_half - (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (hmhalf : m ≤ n / 2) : - (4 : ℝ) / n ≤ 2 * Real.sin (Real.pi * (m : ℝ) / n) := by - have hnR : (0 : ℝ) < n := by exact_mod_cast hn - have hmR : (1 : ℝ) ≤ m := by exact_mod_cast hm - have htwom : 2 * m ≤ n := by omega - have htwomR : (2 : ℝ) * m ≤ n := by exact_mod_cast htwom - have hx0 : (0 : ℝ) ≤ Real.pi * (m : ℝ) / n := by positivity - have hxhalf : Real.pi * (m : ℝ) / n ≤ Real.pi / 2 := by - rw [div_le_iff₀ hnR] - nlinarith [Real.pi_pos] - have hsin := Real.mul_le_sin hx0 hxhalf - have hscale : - (2 : ℝ) * m / n = 2 / Real.pi * (Real.pi * (m : ℝ) / n) := by - field_simp - have hone : (2 : ℝ) / n ≤ 2 * m / n := by - apply (div_le_div_iff_of_pos_right hnR).2 - linarith - have : (2 : ℝ) / n ≤ Real.sin (Real.pi * (m : ℝ) / n) := by - calc - (2 : ℝ) / n ≤ 2 * m / n := hone - _ = 2 / Real.pi * (Real.pi * (m : ℝ) / n) := hscale - _ ≤ Real.sin (Real.pi * (m : ℝ) / n) := hsin - calc - (4 : ℝ) / n = 2 * (2 / n) := by ring - _ ≤ 2 * Real.sin (Real.pi * (m : ℝ) / n) := - mul_le_mul_of_nonneg_left this (by norm_num) - -private lemma four_div_le_norm_one_sub_stdAddChar - (n : ℕ) [NeZero n] (t : ZMod n) (ht : t ≠ 0) : - (4 : ℝ) / n ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ := by - have hn : 0 < n := NeZero.pos n - have hm : 0 < t.val := ZMod.val_pos.mpr ht - have hmn : t.val < n := t.val_lt - rw [norm_one_sub_stdAddChar] - have hsin_nonneg : - 0 ≤ Real.sin (Real.pi * (t.val : ℝ) / n) := by - apply Real.sin_nonneg_of_nonneg_of_le_pi - · positivity - · have hnR : (0 : ℝ) < n := by exact_mod_cast hn - rw [div_le_iff₀ hnR] - have hmnR : (t.val : ℝ) ≤ n := by exact_mod_cast hmn.le - nlinarith [Real.pi_pos] - rw [Real.norm_of_nonneg (mul_nonneg (by norm_num) hsin_nonneg)] - by_cases hhalf : t.val ≤ n / 2 - · exact four_div_le_two_mul_sin_pi_mul_div_of_le_half n t.val hn hm hhalf - · let d := n - t.val - have hd : 0 < d := Nat.sub_pos_of_lt hmn - have hdhalf : d ≤ n / 2 := by - dsimp [d] - omega - have hsin : - Real.sin (Real.pi * (t.val : ℝ) / n) = - Real.sin (Real.pi * (d : ℝ) / n) := by - calc - Real.sin (Real.pi * (t.val : ℝ) / n) = - Real.sin (Real.pi - Real.pi * (t.val : ℝ) / n) := - (Real.sin_pi_sub _).symm - _ = Real.sin (Real.pi * (d : ℝ) / n) := by - congr 1 - dsimp [d] - have hnR : (n : ℝ) ≠ 0 := by positivity - rw [Nat.cast_sub hmn.le] - field_simp - rw [hsin] - exact four_div_le_two_mul_sin_pi_mul_div_of_le_half n d hn hd hdhalf - -private lemma norm_one_add_mul_stdAddChar_sq - (n : ℕ) [NeZero n] (α : ℝ) (t : ZMod n) : - ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ 2 = - (1 + α) ^ 2 - α * ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := by - rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq] - simp [Complex.normSq_add, Complex.normSq_sub, Complex.normSq_mul, - Complex.normSq_ofReal] - rw [show Complex.normSq (ZMod.stdAddChar t) = 1 by - rw [Complex.normSq_eq_norm_sq] - simp] - ring - -private lemma norm_one_add_mul_stdAddChar_le_sqrt - (n : ℕ) [NeZero n] (α : ℝ) (hα : 0 ≤ α) (t : ZMod n) (ht : t ≠ 0) : - ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ≤ - Real.sqrt ((1 + α) ^ 2 - 16 * α / n ^ 2) := by - have hchord := four_div_le_norm_one_sub_stdAddChar n t ht - have hchord_sq : - (16 : ℝ) / n ^ 2 ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := by - have hsquare := pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ 4 / n) hchord 2 - calc - (16 : ℝ) / n ^ 2 = ((4 : ℝ) / n) ^ 2 := by ring - _ ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := hsquare - apply Real.le_sqrt_of_sq_le - rw [norm_one_add_mul_stdAddChar_sq] - calc - (1 + α) ^ 2 - α * ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 - ≤ (1 + α) ^ 2 - α * ((16 : ℝ) / n ^ 2) := - sub_le_sub_left (mul_le_mul_of_nonneg_left hchord_sq hα) _ - _ = (1 + α) ^ 2 - 16 * α / n ^ 2 := by ring - -/-- A uniform squared spectral ratio for all nontrivial Fourier modes. -/ -private noncomputable def shuniaQSq (n : ℕ) (α : ℝ) : ℝ := - 1 - 16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2) - -private lemma shuniaQSq_nonneg - (n : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) : - 0 ≤ shuniaQSq n α := by - have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn - have hnsq : (4 : ℝ) ≤ (n : ℝ) ^ 2 := by nlinarith - have hαsq : 4 * α ≤ (1 + α) ^ 2 := by nlinarith [sq_nonneg (α - 1)] - have hden : (0 : ℝ) < (n : ℝ) ^ 2 * (1 + α) ^ 2 := by positivity - rw [shuniaQSq, sub_nonneg, div_le_one hden] - have hmul := mul_le_mul hnsq hαsq (mul_nonneg (by norm_num) hα) (by norm_num) - nlinarith - -private lemma shuniaQSq_le_exp (n : ℕ) (α : ℝ) : - shuniaQSq n α ≤ - Real.exp (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2))) := by - simpa [shuniaQSq, add_comm] using - Real.add_one_le_exp (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2))) - -/-- The exponent appearing in the uniform decay estimate. -/ -private noncomputable def shuniaDecay (a n : ℕ) (α : ℝ) : ℝ := - 16 * a * α / (n * (1 + α) ^ 2) - -private lemma shuniaQSq_pow_le_exp_neg_decay - (a n : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) : - shuniaQSq n α ^ (a * n) ≤ Real.exp (-shuniaDecay a n α) := by - have hpow := pow_le_pow_left₀ (shuniaQSq_nonneg n hn α hα) - (shuniaQSq_le_exp n α) (a * n) - calc - shuniaQSq n α ^ (a * n) - ≤ Real.exp (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2))) ^ (a * n) := hpow - _ = Real.exp ((a * n : ℕ) * - (-(16 * α / ((n : ℝ) ^ 2 * (1 + α) ^ 2)))) := by - rw [Real.exp_nat_mul] - _ = Real.exp (-shuniaDecay a n α) := by - congr 1 - rw [shuniaDecay] - have hn0 : (n : ℝ) ≠ 0 := by - exact_mod_cast (show n ≠ 0 by omega) - push_cast - field_simp - -private lemma five_thirds_pow_le_two_pow_sub_one (n : ℕ) (hn : 6 ≤ n) : - ((5 : ℝ) / 3) ^ n ≤ 2 ^ (n - 1) := by - induction n, hn using Nat.le_induction with - | base => norm_num - | succ n hn ih => - rw [pow_succ] - calc - ((5 : ℝ) / 3) ^ n * (5 / 3) ≤ 2 ^ (n - 1) * (5 / 3) := - mul_le_mul_of_nonneg_right ih (by norm_num) - _ ≤ 2 ^ (n - 1) * 2 := - mul_le_mul_of_nonneg_left (by norm_num) (by positivity) - _ = 2 ^ (n + 1 - 1) := by - rw [show n + 1 - 1 = (n - 1) + 1 by omega, pow_succ] - -private lemma five_thirds_le_of_root_and_log_bound - (a n : ℕ) (hn : 6 ≤ n) (α : ℝ) (hα : 0 ≤ α) - (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : - (5 : ℝ) / 3 ≤ α := by - have hpow : ((5 : ℝ) / 3) ^ n ≤ α ^ n := by - calc - ((5 : ℝ) / 3) ^ n ≤ 2 ^ (n - 1) := five_thirds_pow_le_two_pow_sub_one n hn - _ ≤ (a : ℝ) := by exact_mod_cast ha - _ = α ^ n := hroot.symm - by_contra h - have hlt : α < (5 : ℝ) / 3 := lt_of_not_ge h - have hstrict : α ^ n < ((5 : ℝ) / 3) ^ n := - pow_lt_pow_left₀ hlt hα (by omega) - exact (not_lt_of_ge hpow hstrict) - -private lemma decay_lower_bound_of_six_le - (a n : ℕ) (hn : 6 ≤ n) (α : ℝ) (hα : 0 ≤ α) - (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : - (25 : ℝ) / 4 * a / (n * α) ≤ shuniaDecay a n α := by - have hα53 := five_thirds_le_of_root_and_log_bound a n hn α hα hroot ha - have hnR : (0 : ℝ) < n := by positivity - have hαpos : 0 < α := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 5 / 3) hα53 - have hlinear : 1 + α ≤ (8 / 5 : ℝ) * α := by linarith - have hsquare : (1 + α) ^ 2 ≤ ((8 / 5 : ℝ) * α) ^ 2 := - pow_le_pow_left₀ (by positivity) hlinear 2 - rw [shuniaDecay] - have hnum : (0 : ℝ) ≤ 16 * a * α := by positivity - calc - (25 : ℝ) / 4 * a / (n * α) = - 16 * a * α / (n * (((8 / 5 : ℝ) * α) ^ 2)) := by - field_simp - ring - _ ≤ 16 * a * α / (n * (1 + α) ^ 2) := by - apply div_le_div_of_nonneg_left hnum - · positivity - · exact mul_le_mul_of_nonneg_left hsquare (by positivity) - -private lemma ten_factorial_poly_lt_two_pow (n : ℕ) (hn : 10 ≤ n) : - 16 * 10 ! * 4 ^ 10 * n ^ 12 < 25 ^ 10 * 2 ^ (7 * (n - 1)) := by - induction n, hn using Nat.le_induction with - | base => norm_num [Nat.factorial] - | succ n hn ih => - have hlinear : 10 * (n + 1) ≤ 11 * n := by omega - have hpow := Nat.pow_le_pow_left hlinear 12 - have hconstant : 11 ^ 12 < 128 * 10 ^ 12 := by norm_num - have hnpos : 0 < n ^ 12 := Nat.pow_pos (by omega) - have hpoly : (n + 1) ^ 12 < 128 * n ^ 12 := by - have hscaled : - 10 ^ 12 * (n + 1) ^ 12 < 10 ^ 12 * (128 * n ^ 12) := by - calc - 10 ^ 12 * (n + 1) ^ 12 = (10 * (n + 1)) ^ 12 := by rw [mul_pow] - _ ≤ (11 * n) ^ 12 := hpow - _ = 11 ^ 12 * n ^ 12 := by rw [mul_pow] - _ < (128 * 10 ^ 12) * n ^ 12 := - Nat.mul_lt_mul_of_pos_right hconstant hnpos - _ = 10 ^ 12 * (128 * n ^ 12) := by ring - omega - let C : ℕ := 16 * 10 ! * 4 ^ 10 - let R : ℕ := 25 ^ 10 * 2 ^ (7 * (n - 1)) - have hC : 0 < C := by - dsimp [C] - positivity - have hstep₁ : C * (n + 1) ^ 12 < 128 * (C * n ^ 12) := by - calc - C * (n + 1) ^ 12 < C * (128 * n ^ 12) := - Nat.mul_lt_mul_of_pos_left hpoly hC - _ = 128 * (C * n ^ 12) := by ring - have hstep₂ : 128 * (C * n ^ 12) < 128 * R := by - apply Nat.mul_lt_mul_of_pos_left - · simpa [C, R] using ih - · norm_num - calc - 16 * 10 ! * 4 ^ 10 * (n + 1) ^ 12 = C * (n + 1) ^ 12 := by rfl - _ < 128 * (C * n ^ 12) := hstep₁ - _ < 128 * R := hstep₂ - _ = 25 ^ 10 * 2 ^ (7 * (n + 1 - 1)) := by - dsimp [R] - rw [show 7 * n = 7 * (n - 1) + 7 by omega, pow_add] - norm_num - ring - -private lemma decay_large_of_ten_le - (a n : ℕ) (hn : 10 ≤ n) (α : ℝ) (hα : 0 ≤ α) - (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : - (16 : ℝ) * n * (n - 1) * a ^ 2 < Real.exp (shuniaDecay a n α) := by - have hn6 : 6 ≤ n := hn.trans' (by norm_num) - have hα53 := five_thirds_le_of_root_and_log_bound a n hn6 α hα hroot ha - have hα1 : (1 : ℝ) ≤ α := le_trans (by norm_num) hα53 - have hαpos : 0 < α := zero_lt_one.trans_le hα1 - have haPos : (0 : ℝ) < a := by - exact_mod_cast (lt_of_lt_of_le (Nat.pow_pos (by decide)) ha) - have hα10 : α ^ 10 ≤ (a : ℝ) := by - calc - α ^ 10 ≤ α ^ n := pow_le_pow_right₀ hα1 hn - _ = (a : ℝ) := hroot - have ha7 : 2 ^ (7 * (n - 1)) ≤ a ^ 7 := by - calc - 2 ^ (7 * (n - 1)) = (2 ^ (n - 1)) ^ 7 := by - rw [show 7 * (n - 1) = (n - 1) * 7 by omega, pow_mul] - _ ≤ a ^ 7 := Nat.pow_le_pow_left ha 7 - have hpolyNat : - 16 * 10 ! * 4 ^ 10 * n ^ 12 < 25 ^ 10 * a ^ 7 := - (ten_factorial_poly_lt_two_pow n hn).trans_le - (Nat.mul_le_mul_left (25 ^ 10) ha7) - have hpoly : - (16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 12 < - (25 : ℝ) ^ 10 * (a : ℝ) ^ 7 := by - exact_mod_cast hpolyNat - have hcross : - ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * α ^ 10) < - (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by - calc - ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * α ^ 10) - ≤ ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 12) * (a : ℝ) ^ 3 := by - have haR : (0 : ℝ) ≤ a := by positivity - calc - ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * α ^ 10) - ≤ ((16 : ℝ) * n * n * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * α ^ 10) := by - gcongr - linarith - _ ≤ ((16 : ℝ) * n * n * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * (a : ℝ)) := by gcongr - _ = ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 12) * (a : ℝ) ^ 3 := by - ring - _ < ((25 : ℝ) ^ 10 * (a : ℝ) ^ 7) * (a : ℝ) ^ 3 := - mul_lt_mul_of_pos_right hpoly (pow_pos haPos 3) - _ = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by ring - let L : ℝ := (25 : ℝ) / 4 * a / (n * α) - have hL0 : 0 ≤ L := by - dsimp [L] - positivity - have hLpow : - L ^ 10 = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 / (4 ^ 10 * n ^ 10 * α ^ 10) := by - dsimp [L] - field_simp - have hterm : - (16 : ℝ) * n * (n - 1) * a ^ 2 < L ^ 10 / (10 ! : ℕ) := by - rw [hLpow] - apply (lt_div_iff₀ (by positivity : (0 : ℝ) < (10 ! : ℕ))).2 - apply (lt_div_iff₀ (by positivity : (0 : ℝ) < 4 ^ 10 * n ^ 10 * α ^ 10)).2 - exact hcross - have hLdecay : L ≤ shuniaDecay a n α := - decay_lower_bound_of_six_le a n hn6 α hα hroot ha - have hdecay0 : 0 ≤ shuniaDecay a n α := hL0.trans hLdecay - calc - (16 : ℝ) * n * (n - 1) * a ^ 2 - < L ^ 10 / (10 ! : ℕ) := hterm - _ ≤ shuniaDecay a n α ^ 10 / (10 ! : ℕ) := by - gcongr - _ ≤ Real.exp (shuniaDecay a n α) := - Real.pow_div_factorial_le_exp (x := shuniaDecay a n α) hdecay0 10 - -private lemma small_n_decay_numeric (n : ℕ) (hn6 : 6 ≤ n) (hn10 : n < 10) : - (16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1) < - 25 ^ 10 * (((2 ^ (n - 1) : ℕ) : ℝ) ^ 6) * - ((5 : ℝ) / 3) ^ (2 * n - 10) := by - interval_cases n <;> norm_num [Nat.factorial] - -private lemma decay_large_of_six_le_of_lt_ten - (a n : ℕ) (hn6 : 6 ≤ n) (hn10 : n < 10) (α : ℝ) (hα : 0 ≤ α) - (hroot : α ^ n = a) (ha : 2 ^ (n - 1) ≤ a) : - (16 : ℝ) * n * (n - 1) * a ^ 2 < Real.exp (shuniaDecay a n α) := by - have hα53 := five_thirds_le_of_root_and_log_bound a n hn6 α hα hroot ha - have hαpos : 0 < α := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 5 / 3) hα53 - have haPos : (0 : ℝ) < a := by - exact_mod_cast (lt_of_lt_of_le (Nat.pow_pos (by decide)) ha) - have ha6 : ((2 ^ (n - 1) : ℕ) : ℝ) ^ 6 ≤ (a : ℝ) ^ 6 := by - exact_mod_cast Nat.pow_le_pow_left ha 6 - have hαrem : - ((5 : ℝ) / 3) ^ (2 * n - 10) ≤ α ^ (2 * n - 10) := - pow_le_pow_left₀ (by norm_num) hα53 _ - have hidentity : - (a : ℝ) ^ 6 * α ^ (2 * n - 10) * α ^ 10 = (a : ℝ) ^ 8 := by - rw [← hroot] - simp only [← pow_mul] - rw [← pow_add, ← pow_add] - congr 1 - omega - have hratio : - ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1)) * α ^ 10 < - 25 ^ 10 * (a : ℝ) ^ 8 := by - calc - ((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1)) * α ^ 10 - < (25 ^ 10 * ((2 ^ (n - 1) : ℕ) : ℝ) ^ 6 * - ((5 : ℝ) / 3) ^ (2 * n - 10)) * α ^ 10 := - mul_lt_mul_of_pos_right (small_n_decay_numeric n hn6 hn10) - (pow_pos hαpos 10) - _ ≤ (25 ^ 10 * (a : ℝ) ^ 6 * α ^ (2 * n - 10)) * α ^ 10 := by - gcongr - _ = 25 ^ 10 * (a : ℝ) ^ 8 := by rw [← hidentity]; ring - have hcross : - ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * α ^ 10) < - (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by - calc - ((16 : ℝ) * n * (n - 1) * (a : ℝ) ^ 2) * (10 ! : ℕ) * - (4 ^ 10 * n ^ 10 * α ^ 10) - = (((16 : ℝ) * (10 ! : ℕ) * 4 ^ 10 * n ^ 11 * (n - 1)) * - α ^ 10) * (a : ℝ) ^ 2 := by ring - _ < (25 ^ 10 * (a : ℝ) ^ 8) * (a : ℝ) ^ 2 := - mul_lt_mul_of_pos_right hratio (pow_pos haPos 2) - _ = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 := by ring - let L : ℝ := (25 : ℝ) / 4 * a / (n * α) - have hL0 : 0 ≤ L := by - dsimp [L] - positivity - have hLpow : - L ^ 10 = (25 : ℝ) ^ 10 * (a : ℝ) ^ 10 / (4 ^ 10 * n ^ 10 * α ^ 10) := by - dsimp [L] - field_simp - have hterm : - (16 : ℝ) * n * (n - 1) * a ^ 2 < L ^ 10 / (10 ! : ℕ) := by - rw [hLpow] - apply (lt_div_iff₀ (by positivity : (0 : ℝ) < (10 ! : ℕ))).2 - apply (lt_div_iff₀ (by positivity : (0 : ℝ) < 4 ^ 10 * n ^ 10 * α ^ 10)).2 - exact hcross - have hLdecay : L ≤ shuniaDecay a n α := - decay_lower_bound_of_six_le a n hn6 α hα hroot ha - have hdecay0 : 0 ≤ shuniaDecay a n α := hL0.trans hLdecay - calc - (16 : ℝ) * n * (n - 1) * a ^ 2 - < L ^ 10 / (10 ! : ℕ) := hterm - _ ≤ shuniaDecay a n α ^ 10 / (10 ! : ℕ) := by gcongr - _ ≤ Real.exp (shuniaDecay a n α) := - Real.pow_div_factorial_le_exp (x := shuniaDecay a n α) hdecay0 10 - -private lemma norm_one_add_mul_stdAddChar_sq_le - (n : ℕ) [NeZero n] (α : ℝ) (hα : 0 ≤ α) (t : ZMod n) (ht : t ≠ 0) : - ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ 2 ≤ - (1 + α) ^ 2 * shuniaQSq n α := by - have hchord := four_div_le_norm_one_sub_stdAddChar n t ht - have hchord_sq : - (16 : ℝ) / n ^ 2 ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := by - have hsquare := pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ 4 / n) hchord 2 - calc - (16 : ℝ) / n ^ 2 = ((4 : ℝ) / n) ^ 2 := by ring - _ ≤ ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 := hsquare - rw [norm_one_add_mul_stdAddChar_sq] - calc - (1 + α) ^ 2 - α * ‖(1 : ℂ) - ZMod.stdAddChar t‖ ^ 2 - ≤ (1 + α) ^ 2 - α * ((16 : ℝ) / n ^ 2) := - sub_le_sub_left (mul_le_mul_of_nonneg_left hchord_sq hα) _ - _ = (1 + α) ^ 2 * shuniaQSq n α := by - rw [shuniaQSq] - have hn : (n : ℝ) ≠ 0 := by exact_mod_cast (NeZero.ne n) - have hα1 : (1 + α : ℝ) ≠ 0 := by positivity - field_simp - -private lemma norm_one_add_mul_stdAddChar_even_pow_le - (a n : ℕ) [NeZero n] (α : ℝ) (hα : 0 ≤ α) (t : ZMod n) (ht : t ≠ 0) : - ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ (2 * a * n) ≤ - (1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n) := by - have hsquare := norm_one_add_mul_stdAddChar_sq_le n α hα t ht - have hpow := pow_le_pow_left₀ (sq_nonneg ‖1 + (α : ℂ) * ZMod.stdAddChar t‖) - hsquare (a * n) - calc - ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ (2 * a * n) = - (‖1 + (α : ℂ) * ZMod.stdAddChar t‖ ^ 2) ^ (a * n) := by - simpa [mul_assoc] using - (pow_mul ‖1 + (α : ℂ) * ZMod.stdAddChar t‖ 2 (a * n)) - _ ≤ ((1 + α) ^ 2 * shuniaQSq n α) ^ (a * n) := hpow - _ = (1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n) := by - rw [mul_pow] - congr 1 - simpa [mul_assoc] using (pow_mul (1 + α) 2 (a * n)).symm - -/-- The relative Fourier-error factor at the exponent `2 * a * n`. -/ -private noncomputable def shuniaError (a n : ℕ) (α : ℝ) : ℝ := - ((n - 1 : ℕ) : ℝ) * shuniaQSq n α ^ (a * n) - -private lemma norm_shuniaScaledCoeff_sub_mainTerm_at_K_le - (a n : ℕ) [NeZero n] (α : ℝ) (hroot : α ^ n = a) (hα : 0 ≤ α) - (i : ZMod n) : - ‖shuniaScaledCoeff a n (2 * a * n) α i - shuniaMainTerm n (2 * a * n) α‖ ≤ - ‖(n : ℂ)⁻¹‖ * (1 + α) ^ (2 * a * n) * shuniaError a n α := by - refine (norm_shuniaScaledCoeff_sub_mainTerm_le_sum - a n (2 * a * n) α hroot i).trans ?_ - have hsum : - ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ (2 * a * n) ≤ - ((n - 1 : ℕ) : ℝ) * - ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n)) := by - calc - ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ (2 * a * n) - ≤ ∑ _t ∈ (Finset.univ.erase (0 : ZMod n)), - ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n)) := by - apply Finset.sum_le_sum - intro t ht - exact norm_one_add_mul_stdAddChar_even_pow_le a n α hα (-t) - (neg_ne_zero.mpr (Finset.ne_of_mem_erase ht)) - _ = ((n - 1 : ℕ) : ℝ) * - ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n)) := by simp - calc - ‖(n : ℂ)⁻¹‖ * ∑ t ∈ (Finset.univ.erase (0 : ZMod n)), - ‖1 + (α : ℂ) * ZMod.stdAddChar (-t)‖ ^ (2 * a * n) - ≤ ‖(n : ℂ)⁻¹‖ * (((n - 1 : ℕ) : ℝ) * - ((1 + α) ^ (2 * a * n) * shuniaQSq n α ^ (a * n))) := - mul_le_mul_of_nonneg_left hsum (norm_nonneg _) - _ = ‖(n : ℂ)⁻¹‖ * (1 + α) ^ (2 * a * n) * shuniaError a n α := by - rw [shuniaError] - ring - -end Nat diff --git a/Mathlib/NumberTheory/ShuniaIntegerRoot.lean b/Mathlib/NumberTheory/ShuniaIntegerRoot.lean new file mode 100644 index 00000000000000..c2900f23e89b08 --- /dev/null +++ b/Mathlib/NumberTheory/ShuniaIntegerRoot.lean @@ -0,0 +1,1219 @@ +/- +Copyright (c) 2026 Ravi Bajaj and Ben Burns. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ravi Bajaj, Ben Burns +-/ +module + +public import Mathlib.NumberTheory.ShuniaIntegerRoot.Estimates +public import Mathlib.Data.Nat.NthRoot.Defs +import Mathlib.Algebra.BigOperators.ModEq +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar +import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas +import Mathlib.Data.Nat.Choose.Sum + +/-! +# Shunia's integer-root formula + +This file proves Conjecture 6.1 from: + +* J. M. Shunia, *Polynomial quotient rings and Kronecker substitution for deriving + combinatorial identities*, arXiv:2404.00332. + +The conjecture gives a fixed-length expression for `Nat.nthRoot n a` in terms of two modular +exponentiations. Its proof uses the coefficients of `(1 + T) ^ k` reduced by the relation +`T ^ n = a`. A roots-of-unity filter shows that adjacent leading coefficients have ratio very +close to the positive real `n`-th root of `a`; evaluation at the large base `a ^ (2 * a * n)` +then recovers that ratio from the two modular residues. +-/ + +@[expose] public section + +open scoped BigOperators + +namespace ShuniaIntegerRoot + +/-- The coefficient of `T ^ i` in `(1 + T) ^ k`, reduced using `T ^ n = a`. -/ +private def coeff (a n k i : ℕ) : ℕ := + ∑ j ∈ Finset.range (k + 1) with j % n = i, k.choose j * a ^ (j / n) + +/-- Evaluation at `x` of `(1 + T) ^ k` reduced using `T ^ n = a`. -/ +private def reducedEval (a n k x : ℕ) : ℕ := + ∑ i ∈ Finset.range n, coeff a n k i * x ^ i + +private lemma coeff_pos_of_lt_of_le {a n k i : ℕ} (hin : i < n) (hik : i ≤ k) : + 0 < coeff a n k i := by + unfold coeff + apply Finset.sum_pos' + · exact fun _ _ ↦ Nat.zero_le _ + · refine ⟨i, ?_, ?_⟩ + · simp [hik, Nat.mod_eq_of_lt hin] + · simpa [Nat.div_eq_of_lt hin] using Nat.choose_pos hik + +private lemma reducedEval_eq_sum_mod (a n k x : ℕ) (hn : 0 < n) : + reducedEval a n k x = + ∑ j ∈ Finset.range (k + 1), k.choose j * a ^ (j / n) * x ^ (j % n) := by + classical + simp only [reducedEval, coeff, Finset.sum_mul, Finset.sum_filter] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro j hj + simp [Nat.mod_lt j hn, mul_assoc] + +private lemma sum_coeff_eq (a n k : ℕ) (hn : 0 < n) : + (∑ i ∈ Finset.range n, coeff a n k i) = + ∑ j ∈ Finset.range (k + 1), k.choose j * a ^ (j / n) := by + simpa [reducedEval] using reducedEval_eq_sum_mod a n k 1 hn + +private lemma reducedEval_le_top_pow_mul_sum {a n k x : ℕ} (hn : 0 < n) (hx : 0 < x) : + reducedEval a n k x ≤ + x ^ (n - 1) * ∑ i ∈ Finset.range n, coeff a n k i := by + unfold reducedEval + calc + (∑ i ∈ Finset.range n, coeff a n k i * x ^ i) ≤ + ∑ i ∈ Finset.range n, coeff a n k i * x ^ (n - 1) := by + apply Finset.sum_le_sum + intro i hi + apply Nat.mul_le_mul_left + exact Nat.pow_le_pow_right hx (by + have := Finset.mem_range.mp hi + omega) + _ = x ^ (n - 1) * ∑ i ∈ Finset.range n, coeff a n k i := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro i hi + exact mul_comm _ _ + +private def lowerEval (c : ℕ → ℕ) (n x : ℕ) : ℕ := + ∑ i ∈ Finset.range (n - 1), c i * x ^ i + +private lemma lowerEval_cast_le + {a n x : ℕ} {α : ℝ} {c : ℕ → ℕ} + (hn : 1 < n) (hx : 0 < x) (hα : 1 ≤ α) (hαpow : α ^ n = a) + (hC : 0 < c (n - 1)) + (hrel : ∀ i < n - 1, + (c i : ℝ) / (c (n - 1) : ℝ) < 2 * α ^ (n - 1 - i)) : + (lowerEval c n x : ℝ) ≤ 2 * n * a * c (n - 1) * x ^ (n - 2) := by + have hC' : (0 : ℝ) < c (n - 1) := by exact_mod_cast hC + rw [lowerEval] + push_cast + calc + (∑ i ∈ Finset.range (n - 1), (c i : ℝ) * (x : ℝ) ^ i) ≤ + ∑ _i ∈ Finset.range (n - 1), + (2 * (a : ℝ) * c (n - 1) * (x : ℝ) ^ (n - 2)) := by + apply Finset.sum_le_sum + intro i hi + have hi' := Finset.mem_range.mp hi + have hci : (c i : ℝ) ≤ 2 * α ^ (n - 1 - i) * c (n - 1) := + ((div_lt_iff₀ hC').mp (hrel i hi')).le + have hαi : α ^ (n - 1 - i) ≤ (a : ℝ) := by + calc + α ^ (n - 1 - i) ≤ α ^ n := pow_le_pow_right₀ hα (by omega) + _ = a := hαpow + have hxi : (x : ℝ) ^ i ≤ (x : ℝ) ^ (n - 2) := + pow_le_pow_right₀ (by exact_mod_cast (show 1 ≤ x by omega)) (by omega) + calc + (c i : ℝ) * x ^ i ≤ (2 * α ^ (n - 1 - i) * c (n - 1)) * x ^ i := by + gcongr + _ ≤ (2 * (a : ℝ) * c (n - 1)) * x ^ (n - 2) := by gcongr + _ = (n - 1 : ℕ) * (2 * (a : ℝ) * c (n - 1) * x ^ (n - 2)) := by simp + _ ≤ n * (2 * (a : ℝ) * c (n - 1) * x ^ (n - 2)) := by gcongr; omega + _ = 2 * n * a * c (n - 1) * x ^ (n - 2) := by ring + +private lemma lowerEval_error_le + {a n x : ℕ} {α : ℝ} {c : ℕ → ℕ} + (hn : 1 < n) (hx : 0 < x) (hα : 1 ≤ α) (hαpow : α ^ n = a) + (hC : 0 < c (n - 1)) + (hrel : ∀ i < n - 1, + (c i : ℝ) / (c (n - 1) : ℝ) < 2 * α ^ (n - 1 - i)) : + (lowerEval c n x : ℝ) / ((c (n - 1) : ℝ) * x ^ (n - 1)) ≤ 2 * n * a / x := by + have hC' : (0 : ℝ) < c (n - 1) := by exact_mod_cast hC + have hx' : (0 : ℝ) < x := by exact_mod_cast hx + rw [div_le_iff₀ (mul_pos hC' (pow_pos hx' _))] + calc + (lowerEval c n x : ℝ) ≤ 2 * n * a * c (n - 1) * x ^ (n - 2) := + lowerEval_cast_le hn hx hα hαpow hC hrel + _ = (2 * n * a / x) * ((c (n - 1) : ℝ) * x ^ (n - 1)) := by + rw [show n - 1 = n - 2 + 1 by omega, pow_succ] + field_simp + +private lemma ratio_leading_error + {U C Y L L' B Q : ℝ} + (hU : 0 < U) (hC : 0 < C) (hY : 0 < Y) + (hL : 0 ≤ L) (hL' : 0 ≤ L') (hB : 0 ≤ B) + (heD : L / (U * Y) ≤ B) (heN : L' / (C * Y) ≤ B) + (hCU : C / U ≤ Q) : + |(C * Y + L') / (U * Y + L) - C / U| ≤ Q * B := by + let eD := L / (U * Y) + let eN := L' / (C * Y) + have heD0 : 0 ≤ eD := div_nonneg hL (mul_pos hU hY).le + have heN0 : 0 ≤ eN := div_nonneg hL' (mul_pos hC hY).le + have heDB : eD ≤ B := heD + have heNB : eN ≤ B := heN + have hden : 0 < 1 + eD := by linarith + have hDY : U * Y + L = U * Y * (1 + eD) := by + dsimp [eD] + field_simp + have hNY : C * Y + L' = C * Y * (1 + eN) := by + dsimp [eN] + field_simp + have hratio : + (C * Y + L') / (U * Y + L) - C / U = + (C / U) * ((eN - eD) / (1 + eD)) := by + rw [hDY, hNY] + field_simp [ne_of_gt hU, ne_of_gt hC, ne_of_gt hY, ne_of_gt hden] + ring + have hdiff : |eN - eD| ≤ B := by rw [abs_le]; constructor <;> linarith + have hfrac : |(eN - eD) / (1 + eD)| ≤ B := by + rw [abs_div, abs_of_pos hden] + exact (div_le_div_of_nonneg_right hdiff hden.le).trans + (div_le_self hB (by linarith)) + rw [hratio, abs_mul, abs_of_pos (div_pos hC hU)] + exact (mul_le_mul_of_nonneg_left hfrac (div_pos hC hU).le).trans + (mul_le_mul_of_nonneg_right hCU hB) + +private lemma sixteen_mul_sq_mul_pow_four_lt_pow + {a n K : ℕ} (ha : 4 ≤ a) (hna : n ≤ a) (hK : 16 ≤ K) : + 16 * n ^ 2 * a ^ 4 < a ^ K := by + have ha0 : 0 < a := by omega + have hpoly : 16 * n ^ 2 * a ^ 4 ≤ 16 * a ^ 6 := by + calc + 16 * n ^ 2 * a ^ 4 ≤ 16 * a ^ 2 * a ^ 4 := by + gcongr + _ = 16 * a ^ 6 := by ring + have hp10 : 16 < a ^ 10 := + (by norm_num : 16 < 4 ^ 10).trans_le (Nat.pow_le_pow_left ha 10) + have hp16 : 16 * a ^ 6 < a ^ 16 := by + calc + 16 * a ^ 6 < a ^ 10 * a ^ 6 := Nat.mul_lt_mul_of_pos_right hp10 (pow_pos ha0 _) + _ = a ^ 16 := by ring + exact hpoly.trans_lt <| hp16.trans_le (Nat.pow_le_pow_right ha0 hK) + +private lemma leading_recovery_of_decomposition + {a n x : ℕ} {α : ℝ} {c d : ℕ → ℕ} + (ha : 4 ≤ a) (hn : 1 < n) (hna : n ≤ a) + (hα : 1 < α) (hαpow : α ^ n = a) + (hU : 0 < c (n - 1)) (hC : 0 < d (n - 1)) + (hrelc : ∀ i < n - 1, + (c i : ℝ) / (c (n - 1) : ℝ) < 2 * α ^ (n - 1 - i)) + (hreld : ∀ i < n - 1, + (d i : ℝ) / (d (n - 1) : ℝ) < 2 * α ^ (n - 1 - i)) + (hCU : (d (n - 1) : ℝ) / c (n - 1) < 2 * a) + (hx : x = a ^ (2 * a * n)) : + |((d (n - 1) * x ^ (n - 1) + lowerEval d n x : ℕ) : ℝ) / + ((c (n - 1) * x ^ (n - 1) + lowerEval c n x : ℕ) : ℝ) - + (d (n - 1) : ℝ) / c (n - 1)| < α / (4 * n * a ^ 2) := by + have hx0 : 0 < x := by simp [hx, show 0 < a by omega] + have hxbigNat : 16 * n ^ 2 * a ^ 4 < x := by + rw [hx] + exact sixteen_mul_sq_mul_pow_four_lt_pow ha hna (by nlinarith) + have hxbig : (16 : ℝ) * n ^ 2 * a ^ 4 < x := by exact_mod_cast hxbigNat + have hec := lowerEval_error_le hn hx0 hα.le hαpow hU hrelc + have hed := lowerEval_error_le hn hx0 hα.le hαpow hC hreld + have hratio := ratio_leading_error + (U := (c (n - 1) : ℝ)) (C := (d (n - 1) : ℝ)) (Y := (x : ℝ) ^ (n - 1)) + (L := (lowerEval c n x : ℝ)) (L' := (lowerEval d n x : ℝ)) + (B := 2 * n * a / x) (Q := 2 * a) + (by exact_mod_cast hU) (by exact_mod_cast hC) (by positivity) + (by positivity) (by positivity) (by positivity) hec hed hCU.le + push_cast at hratio ⊢ + have hcoarse : (2 * (a : ℝ)) * (2 * n * a / x) < α / (4 * n * a ^ 2) := by + have hxR : (0 : ℝ) < x := by positivity + rw [show (2 * (a : ℝ)) * (2 * n * a / x) = (4 * n * a ^ 2) / x by ring, + div_lt_div_iff₀ hxR (by positivity)] + have : (16 : ℝ) * n ^ 2 * a ^ 4 < α * x := + hxbig.trans_le (by nlinarith) + nlinarith + exact hratio.trans_lt hcoarse + +private theorem eval_ratio_close_leading_ratio + {a n : ℕ} {α : ℝ} (c d : ℕ → ℕ) + (ha : 4 ≤ a) (hn : 1 < n) (hna : n ≤ a) + (hα : 1 < α) (hαpow : α ^ n = a) + (hU : 0 < c (n - 1)) (hC : 0 < d (n - 1)) + (hrelc : ∀ i < n - 1, + (c i : ℝ) / (c (n - 1) : ℝ) < 2 * α ^ (n - 1 - i)) + (hreld : ∀ i < n - 1, + (d i : ℝ) / (d (n - 1) : ℝ) < 2 * α ^ (n - 1 - i)) + (hCU : (d (n - 1) : ℝ) / c (n - 1) < 2 * a) : + let x := a ^ (2 * a * n) + |((∑ i ∈ Finset.range n, d i * x ^ i : ℕ) : ℝ) / + ((∑ i ∈ Finset.range n, c i * x ^ i : ℕ) : ℝ) - + (d (n - 1) : ℝ) / c (n - 1)| < α / (4 * n * a ^ 2) := by + dsimp only + let x := a ^ (2 * a * n) + change + |((∑ i ∈ Finset.range n, d i * x ^ i : ℕ) : ℝ) / + ((∑ i ∈ Finset.range n, c i * x ^ i : ℕ) : ℝ) - + (d (n - 1) : ℝ) / c (n - 1)| < α / (4 * n * a ^ 2) + have hsplit (f : ℕ → ℕ) : + (∑ i ∈ Finset.range n, f i * x ^ i) = + f (n - 1) * x ^ (n - 1) + lowerEval f n x := by + rw [show n = n - 1 + 1 by omega, Finset.sum_range_succ, add_comm] + rfl + rw [hsplit d, hsplit c] + exact leading_recovery_of_decomposition ha hn hna hα hαpow hU hC + hrelc hreld hCU rfl + +private lemma pow_modEq_reduced_term {a n x m j : ℕ} + (hax : x ^ n ≡ a [MOD m]) : + x ^ j ≡ a ^ (j / n) * x ^ (j % n) [MOD m] := by + have hpow : (x ^ n) ^ (j / n) ≡ a ^ (j / n) [MOD m] := hax.pow _ + have hmul := hpow.mul (Nat.ModEq.refl (x ^ (j % n))) + rw [← pow_mul, ← pow_add] at hmul + simpa [Nat.div_add_mod j n] using hmul + +private lemma add_one_pow_modEq_reducedEval {a n k x m : ℕ} (hn : 0 < n) + (hax : x ^ n ≡ a [MOD m]) : + (x + 1) ^ k ≡ reducedEval a n k x [MOD m] := by + rw [add_pow, reducedEval_eq_sum_mod a n k x hn] + apply Nat.ModEq.sum + intro j hj + simpa [mul_assoc, mul_comm, mul_left_comm] using + (pow_modEq_reduced_term (j := j) hax).mul_left (k.choose j) + +private lemma add_one_pow_mod_eq_reducedEval {a n k x : ℕ} (hn : 0 < n) + (ha : a ≤ x ^ n) (hsmall : reducedEval a n k x < x ^ n - a) : + (x + 1) ^ k % (x ^ n - a) = reducedEval a n k x := by + exact ((Nat.mod_modEq _ _).trans + (add_one_pow_modEq_reducedEval (k := k) hn (Nat.modEq_sub ha))).eq_of_lt_of_lt + (Nat.mod_lt _ (Nat.zero_lt_of_lt hsmall)) hsmall + +private def weight (a n i j : ℕ) : ℕ := + if j % n = i then a ^ (j / n) else 0 + +private lemma coeff_eq_sum_weight (a n k i : ℕ) : + coeff a n k i = + ∑ j ∈ Finset.range (k + 1), k.choose j * weight a n i j := by + simp only [coeff, weight] + rw [Finset.sum_filter] + apply Finset.sum_congr rfl + intro j hj + split_ifs <;> simp_all + +private lemma coeff_succ (a n k i : ℕ) : + coeff a n (k + 1) i = + coeff a n k i + + ∑ j ∈ Finset.range (k + 1), k.choose j * weight a n i (j + 1) := by + rw [coeff_eq_sum_weight, coeff_eq_sum_weight] + simpa using Finset.sum_choose_succ_mul (R := ℕ) (fun j _ ↦ weight a n i j) k + +private lemma weight_top_succ {a n j : ℕ} (hn : 1 < n) : + weight a n (n - 1) (j + 1) = weight a n (n - 2) j := by + unfold weight + have hn0 : 0 < n := by omega + have hmod : (j + 1) % n = n - 1 ↔ j % n = n - 2 := by + rw [Nat.add_mod] + rw [Nat.mod_eq_of_lt hn] + have hjmod : j % n < n := Nat.mod_lt _ hn0 + by_cases hlt : j % n + 1 < n + · rw [Nat.mod_eq_of_lt hlt] + omega + · have heq : j % n + 1 = n := by omega + rw [heq, Nat.mod_self] + omega + by_cases h : j % n = n - 2 + · rw [if_pos h, if_pos (hmod.mpr h)] + congr 1 + have hlt : j % n + 1 < n := by omega + have hdiv := Nat.add_div_eq_of_add_mod_lt + (a := j) (b := 1) (c := n) (by simpa [Nat.mod_eq_of_lt hn] using hlt) + simpa [Nat.div_eq_of_lt hn] using hdiv + · rw [if_neg h, if_neg (hmod.not.mpr h)] + +private lemma coeff_succ_top {a n k : ℕ} (hn : 1 < n) : + coeff a n (k + 1) (n - 1) = + coeff a n k (n - 1) + coeff a n k (n - 2) := by + rw [coeff_succ, coeff_eq_sum_weight] + congr 1 + rw [coeff_eq_sum_weight] + apply Finset.sum_congr rfl + intro j hj + rw [weight_top_succ hn] + +private lemma four_mul_le_two_pow {a : ℕ} (ha : 4 ≤ a) : 4 * a ≤ 2 ^ a := by + obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le ha + induction d with + | zero => norm_num + | succ d ih => + rw [show 4 + (d + 1) = (4 + d) + 1 by omega, pow_succ] + have hpos : 1 ≤ 4 + d := by omega + omega + +/-- The positive real `n`-th root used in the spectral argument. -/ +private noncomputable def root (a n : ℕ) : ℝ := (a : ℝ) ^ (n : ℝ)⁻¹ + +private lemma root_pos {a n : ℕ} (ha : 0 < a) : 0 < root a n := by + exact Real.rpow_pos_of_pos (by exact_mod_cast ha) _ + +private lemma root_pow {a n : ℕ} (ha : 0 < a) (hn : n ≠ 0) : + root a n ^ n = a := by + exact Real.rpow_inv_natCast_pow (by positivity : (0 : ℝ) ≤ a) hn + +private lemma weighted_stdAddChar_sum {n i j : ℕ} [NeZero n] (hi : i < n) : + ∑ l : ZMod n, + ZMod.stdAddChar (-((i : ZMod n) * l)) * ZMod.stdAddChar l ^ j = + if j % n = i then (n : ℂ) else 0 := by + calc + _ = ∑ l : ZMod n, + ZMod.stdAddChar (((j : ZMod n) - (i : ZMod n)) * l) := by + apply Finset.sum_congr rfl + intro l hl + rw [← AddChar.map_nsmul_eq_pow, ← AddChar.map_add_eq_mul] + congr 1 + ring + _ = if (j : ZMod n) - (i : ZMod n) = 0 then (n : ℂ) else 0 := by + simpa [mul_comm, ZMod.card] using + AddChar.sum_mulShift ((j : ZMod n) - (i : ZMod n)) + (ZMod.isPrimitive_stdAddChar n) + _ = if j % n = i then (n : ℂ) else 0 := by + split_ifs <;> + simp_all [sub_eq_zero, ZMod.natCast_eq_natCast_iff', Nat.mod_eq_of_lt hi] + +private lemma spectral_sum_eq_filtered + (_a n k i : ℕ) (α : ℝ) [NeZero n] (hi : i < n) : + ∑ l : ZMod n, + ZMod.stdAddChar (-((i : ZMod n) * l)) * + (1 + (α : ℂ) * ZMod.stdAddChar l) ^ k = + (n : ℂ) * + ∑ j ∈ Finset.range (k + 1) with j % n = i, + (k.choose j : ℂ) * (α : ℂ) ^ j := by + have hbin (z : ℂ) : + (1 + z) ^ k = ∑ j ∈ Finset.range (k + 1), (k.choose j : ℂ) * z ^ j := by + rw [add_comm, add_pow] + apply Finset.sum_congr rfl + intro j hj + simp [mul_comm] + calc + _ = ∑ l : ZMod n, + ZMod.stdAddChar (-((i : ZMod n) * l)) * + ∑ j ∈ Finset.range (k + 1), + (k.choose j : ℂ) * ((α : ℂ) * ZMod.stdAddChar l) ^ j := by + apply Finset.sum_congr rfl + intro l hl + rw [hbin] + _ = ∑ j ∈ Finset.range (k + 1), + ((k.choose j : ℂ) * (α : ℂ) ^ j) * + ∑ l : ZMod n, + ZMod.stdAddChar (-((i : ZMod n) * l)) * ZMod.stdAddChar l ^ j := by + simp_rw [Finset.mul_sum] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro j hj + apply Finset.sum_congr rfl + intro l hl + rw [mul_pow] + ring + _ = ∑ j ∈ Finset.range (k + 1), + ((k.choose j : ℂ) * (α : ℂ) ^ j) * + (if j % n = i then (n : ℂ) else 0) := by + apply Finset.sum_congr rfl + intro j hj + rw [weighted_stdAddChar_sum hi] + _ = _ := by + rw [Finset.sum_filter, Finset.mul_sum] + apply Finset.sum_congr rfl + intro j hj + split_ifs <;> ring + +private lemma filtered_sum_eq_coeff_mul + (a n k i : ℕ) (α : ℝ) (hα : α ^ n = (a : ℝ)) : + ∑ j ∈ Finset.range (k + 1) with j % n = i, + (k.choose j : ℂ) * (α : ℂ) ^ j = + (coeff a n k i : ℂ) * (α : ℂ) ^ i := by + rw [coeff, Nat.cast_sum, Finset.sum_mul] + apply Finset.sum_congr rfl + intro j hj + have hjmod : j % n = i := (Finset.mem_filter.mp hj).2 + have hjdiv : n * (j / n) + i = j := by + rw [← hjmod, Nat.div_add_mod] + have hαc : (α : ℂ) ^ n = (a : ℂ) := by exact_mod_cast hα + have hpow : (α : ℂ) ^ j = (a : ℂ) ^ (j / n) * (α : ℂ) ^ i := by + calc + (α : ℂ) ^ j = (α : ℂ) ^ (n * (j / n) + i) := by rw [hjdiv] + _ = ((α : ℂ) ^ n) ^ (j / n) * (α : ℂ) ^ i := by rw [pow_add, pow_mul] + _ = _ := by rw [hαc] + rw [hpow] + push_cast + ring + +private lemma coeff_spectral_identity + (a n k i : ℕ) (α : ℝ) [NeZero n] (hi : i < n) + (hα : α ^ n = (a : ℝ)) : + (n : ℂ) * (coeff a n k i : ℂ) * (α : ℂ) ^ i = + ∑ l : ZMod n, + ZMod.stdAddChar (-((i : ZMod n) * l)) * + (1 + (α : ℂ) * ZMod.stdAddChar l) ^ k := by + rw [spectral_sum_eq_filtered a n k i α hi, filtered_sum_eq_coeff_mul a n k i α hα] + ring + +private lemma sin_pi_div_le_sin_mul {n r : ℕ} (hn : 0 < n) (hr : 0 < r) + (hrhalf : 2 * r ≤ n) : + Real.sin (Real.pi / n) ≤ Real.sin (Real.pi * r / n) := by + have hn0 : (0 : ℝ) < n := by exact_mod_cast hn + apply Real.sin_le_sin_of_le_of_le_pi_div_two + · have : 0 ≤ Real.pi / (n : ℝ) := by positivity + linarith [Real.pi_pos] + · have hrhalf' : (2 : ℝ) * r ≤ n := by exact_mod_cast hrhalf + apply (div_le_iff₀ hn0).2 + nlinarith [Real.pi_pos] + · apply (div_le_div_iff_of_pos_right hn0).2 + have hr' : (1 : ℝ) ≤ r := by exact_mod_cast hr + nlinarith [Real.pi_pos] + +private lemma norm_one_sub_stdAddChar {n : ℕ} [NeZero n] (l : ZMod n) : + ‖(1 : ℂ) - ZMod.stdAddChar l‖ = + 2 * |Real.sin (Real.pi * (l.val : ℝ) / n)| := by + rw [norm_sub_rev, ZMod.stdAddChar_apply, ZMod.toCircle_apply] + have harg : + (2 : ℂ) * Real.pi * Complex.I * (l.val : ℂ) / (n : ℂ) = + Complex.I * ((2 * Real.pi * (l.val : ℝ) / n : ℝ) : ℂ) := by + push_cast + ring + rw [harg, Complex.norm_exp_I_mul_ofReal_sub_one, Real.norm_eq_abs] + rw [show (2 * Real.pi * (l.val : ℝ) / n : ℝ) / 2 = + Real.pi * (l.val : ℝ) / n by ring] + rw [abs_mul, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)] + +private lemma norm_one_add_mul_sq (α : ℝ) (z : ℂ) (hz : ‖z‖ = 1) : + ‖(1 : ℂ) + (α : ℂ) * z‖ ^ 2 = + (1 + α) ^ 2 - α * ‖(1 : ℂ) - z‖ ^ 2 := by + rw [Complex.sq_norm, Complex.sq_norm, Complex.normSq_apply, Complex.normSq_apply] + have hzsq := Complex.sq_norm z + rw [hz, one_pow, Complex.normSq_apply] at hzsq + simp only [Complex.add_re, Complex.one_re, Complex.mul_re, Complex.ofReal_re, + Complex.ofReal_im, zero_mul, sub_zero, Complex.add_im, Complex.one_im, + zero_add, Complex.sub_re, Complex.sub_im, Complex.mul_im, zero_add] + linear_combination -(α + α ^ 2) * hzsq + +private lemma sin_pi_div_le_abs_sin_val_of_two_le {n : ℕ} [NeZero n] (hn : 2 ≤ n) + (l : ZMod n) (hl : l ≠ 0) : + Real.sin (Real.pi / n) ≤ + |Real.sin (Real.pi * (l.val : ℝ) / n)| := by + have hn0 : 0 < n := by omega + have hv0 : 0 < l.val := ZMod.val_pos.mpr hl + have hvn : l.val < n := ZMod.val_lt l + by_cases hvhalf : 2 * l.val ≤ n + · exact (sin_pi_div_le_sin_mul hn0 hv0 hvhalf).trans (le_abs_self _) + · have hr0 : 0 < n - l.val := Nat.sub_pos_of_lt hvn + have hrhalf : 2 * (n - l.val) ≤ n := by omega + have hs := sin_pi_div_le_sin_mul hn0 hr0 hrhalf + have hn0r : (0 : ℝ) < n := by exact_mod_cast hn0 + have hang : + Real.pi * ((n - l.val : ℕ) : ℝ) / n = + Real.pi - Real.pi * (l.val : ℝ) / n := by + rw [Nat.cast_sub hvn.le] + field_simp + rw [hang, Real.sin_pi_sub] at hs + exact hs.trans (le_abs_self _) + +private lemma norm_one_add_stdAddChar_le_spectralRatio {n : ℕ} [NeZero n] + (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) (l : ZMod n) (hl : l ≠ 0) : + ‖(1 : ℂ) + (α : ℂ) * ZMod.stdAddChar l‖ ≤ + (Real.sqrt (1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / n)) / + (1 + α)) * (1 + α) := by + have hnR : (0 : ℝ) < n := by positivity + have hangle0 : 0 < Real.pi / (n : ℝ) := div_pos Real.pi_pos hnR + have hanglePi : Real.pi / (n : ℝ) < Real.pi := by + apply (div_lt_iff₀ hnR).2 + have hnOne : (1 : ℝ) < n := by exact_mod_cast (show 1 < n by omega) + nlinarith [Real.pi_pos] + have hsin0 : 0 ≤ Real.sin (Real.pi / n) := + (Real.sin_pos_of_pos_of_lt_pi hangle0 hanglePi).le + have hdist : + 2 * Real.sin (Real.pi / n) ≤ + ‖(1 : ℂ) - ZMod.stdAddChar l‖ := by + rw [norm_one_sub_stdAddChar] + exact mul_le_mul_of_nonneg_left + (sin_pi_div_le_abs_sin_val_of_two_le hn l hl) (by norm_num) + have hdistsq : + (2 * Real.sin (Real.pi / n)) ^ 2 ≤ + ‖(1 : ℂ) - ZMod.stdAddChar l‖ ^ 2 := + pow_le_pow_left₀ (mul_nonneg (by norm_num) hsin0) hdist 2 + let R : ℝ := 1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / n) + have hnormsq : + ‖(1 : ℂ) + (α : ℂ) * ZMod.stdAddChar l‖ ^ 2 ≤ R := by + rw [norm_one_add_mul_sq α _ (AddChar.norm_apply ZMod.stdAddChar l)] + have hmul := mul_le_mul_of_nonneg_left hdistsq hα + have htrig : + (1 + α) ^ 2 - α * (2 * Real.sin (Real.pi / n)) ^ 2 = R := by + dsimp [R] + rw [show 2 * Real.pi / (n : ℝ) = 2 * (Real.pi / n) by ring, + mul_pow, Real.sin_sq_eq_half_sub] + ring + rw [← htrig] + linarith + have hR0 : 0 ≤ R := (sq_nonneg _).trans hnormsq + have hsqrt : + ‖(1 : ℂ) + (α : ℂ) * ZMod.stdAddChar l‖ ≤ Real.sqrt R := by + apply (sq_le_sq₀ (norm_nonneg _) (Real.sqrt_nonneg _)).mp + rwa [Real.sq_sqrt hR0] + have hden : 0 < 1 + α := by linarith + calc + ‖(1 : ℂ) + (α : ℂ) * ZMod.stdAddChar l‖ ≤ Real.sqrt R := hsqrt + _ = (Real.sqrt R / (1 + α)) * (1 + α) := by field_simp + _ = _ := by rfl + +private noncomputable def spectralRatio (a n : ℕ) : ℝ := + Real.sqrt + (1 + root a n ^ 2 + + 2 * root a n * Real.cos (2 * Real.pi / n)) / + (1 + root a n) + +private lemma spectralRatio_mem_Icc {a n : ℕ} (ha : 0 < a) : + spectralRatio a n ∈ Set.Icc 0 1 := by + constructor + · unfold spectralRatio + exact div_nonneg (Real.sqrt_nonneg _) (by nlinarith [root_pos (n := n) ha]) + · let α := root a n + let R := 1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / n) + have hα : 0 ≤ α := (root_pos (n := n) ha).le + have hden : 0 < 1 + α := by linarith + have hRle : R ≤ (1 + α) ^ 2 := by + have hc := Real.cos_le_one (2 * Real.pi / (n : ℝ)) + dsimp [R] + nlinarith + have hsqrt : Real.sqrt R ≤ 1 + α := + (Real.sqrt_le_iff.mpr ⟨hden.le, hRle⟩) + unfold spectralRatio + change Real.sqrt R / (1 + α) ≤ 1 + exact (div_le_one hden).2 hsqrt + +private lemma one_lt_root {a n : ℕ} (ha : 1 < a) (hn : 0 < n) : 1 < root a n := by + exact Real.one_lt_rpow (by exact_mod_cast ha) (by positivity) + +private lemma root_le_sqrt {a n : ℕ} (ha : 1 ≤ a) (hn : 2 ≤ n) : + root a n ≤ √a := by + rw [root, Real.sqrt_eq_rpow, one_div] + apply Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast ha) + exact inv_anti₀ (by norm_num : (0 : ℝ) < 2) (by exact_mod_cast hn) + +private lemma nthRoot_lt_root {a n : ℕ} (ha : 0 < a) (hn : n ≠ 0) + (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) : + (n.nthRoot a : ℝ) < root a n := by + have hle : n.nthRoot a ^ n ≤ a := Nat.pow_nthRoot_le (.inl hn) + have hne : n.nthRoot a ^ n ≠ a := fun h ↦ hnotpow ⟨n.nthRoot a, h⟩ + have hlt : n.nthRoot a ^ n < a := lt_of_le_of_ne hle hne + have hlt' : (n.nthRoot a : ℝ) ^ n < (a : ℝ) := by exact_mod_cast hlt + rw [← root_pow ha hn] at hlt' + exact (pow_lt_pow_iff_left₀ (by positivity) (root_pos ha).le hn).mp hlt' + +private lemma root_lt_nthRoot_add_one {a n : ℕ} (ha : 0 < a) (hn : n ≠ 0) : + root a n < n.nthRoot a + 1 := by + have hlt := Nat.lt_pow_nthRoot_add_one hn a + have hlt' : (a : ℝ) < ((n.nthRoot a + 1 : ℕ) : ℝ) ^ n := by exact_mod_cast hlt + rw [← root_pow ha hn] at hlt' + push_cast at hlt' + exact (pow_lt_pow_iff_left₀ (root_pos ha).le (by positivity) hn).mp hlt' + +private lemma root_le_nat {a n : ℕ} (ha : 1 < a) (hn : 0 < n) : + root a n ≤ a := by + calc + root a n = root a n ^ 1 := by simp + _ ≤ root a n ^ n := pow_le_pow_right₀ (one_lt_root ha hn).le hn + _ = a := root_pow (by omega) hn.ne' + +private lemma cast_sum_coeff_le {a n k : ℕ} (ha : 1 < a) (hn : 0 < n) : + (∑ i ∈ Finset.range n, coeff a n k i : ℕ) ≤ (1 + root a n) ^ k := by + rw [sum_coeff_eq a n k hn, + show (1 + root a n) ^ k = (root a n + 1) ^ k by rw [add_comm], add_pow] + push_cast + apply Finset.sum_le_sum + intro j hj + simp only [one_pow, mul_one] + ring_nf + apply mul_le_mul_of_nonneg_left _ (by positivity) + calc + ((a : ℝ) ^ (j / n)) = (root a n ^ n) ^ (j / n) := by + rw [root_pow (by omega) hn.ne'] + _ = root a n ^ (n * (j / n)) := by rw [pow_mul] + _ ≤ root a n ^ j := + pow_le_pow_right₀ (one_lt_root ha hn).le (Nat.mul_div_le j n) + +private lemma coeff_normalized_close {a n k i : ℕ} + (ha : 4 ≤ a) (hn : 1 < n) (hpow : 2 ^ (n - 1) ≤ a) + (hi : i < n) (hk : 2 * a * n ≤ k) : + |((n : ℝ) * coeff a n k i * root a n ^ i) / (1 + root a n) ^ k - 1| < + 1 / (16 * (n : ℝ) * a ^ 2) := by + classical + letI : NeZero n := ⟨by omega⟩ + let α := root a n + let q := spectralRatio a n + let f : ZMod n → ℂ := fun l ↦ + ZMod.stdAddChar (-((i : ZMod n) * l)) * + (1 + (α : ℂ) * ZMod.stdAddChar l) ^ k + have ha0 : 0 < a := by omega + have hα0 : 0 < α := root_pos (n := n) ha0 + have hroot : α ^ n = (a : ℝ) := root_pow ha0 (by omega) + have hid := coeff_spectral_identity a n k i α hi hroot + have hf0 : f 0 = ((1 + α) ^ k : ℝ) := by + simp [f] + have hsum : + ∑ l ∈ (Finset.univ.erase (0 : ZMod n)), f l = + ((n : ℝ) * coeff a n k i * α ^ i - (1 + α) ^ k : ℝ) := by + calc + ∑ l ∈ (Finset.univ.erase (0 : ZMod n)), f l = + (∑ l : ZMod n, f l) - f 0 := by + rw [← Finset.add_sum_erase Finset.univ f (Finset.mem_univ 0)] + ring + _ = ((n : ℂ) * (coeff a n k i : ℂ) * (α : ℂ) ^ i) - + ((1 + α) ^ k : ℝ) := by rw [← hid, hf0] + _ = ((n : ℝ) * coeff a n k i * α ^ i - (1 + α) ^ k : ℝ) := by + push_cast + ring + have hterm (l : ZMod n) (hl : l ≠ 0) : + ‖f l‖ ≤ q ^ k * (1 + α) ^ k := by + have hnorm : + ‖(1 : ℂ) + (α : ℂ) * ZMod.stdAddChar l‖ ≤ q * (1 + α) := by + simpa [q, spectralRatio, α] using + norm_one_add_stdAddChar_le_spectralRatio + (n := n) (by omega : 2 ≤ n) α hα0.le l hl + calc + ‖f l‖ = ‖(1 : ℂ) + (α : ℂ) * ZMod.stdAddChar l‖ ^ k := by + simp [f] + _ ≤ (q * (1 + α)) ^ k := + pow_le_pow_left₀ (norm_nonneg _) hnorm k + _ = q ^ k * (1 + α) ^ k := by rw [mul_pow] + have hnormSum : + ‖∑ l ∈ (Finset.univ.erase (0 : ZMod n)), f l‖ ≤ + (n - 1 : ℕ) * (q ^ k * (1 + α) ^ k) := by + have h := norm_sum_le_of_le (Finset.univ.erase (0 : ZMod n)) + (fun l hl ↦ hterm l (Finset.ne_of_mem_erase hl)) + simpa [Finset.card_erase_of_mem (Finset.mem_univ (0 : ZMod n)), ZMod.card] using h + have hqBounds := spectralRatio_mem_Icc (n := n) ha0 + have hqPow : q ^ k ≤ q ^ (2 * a * n) := + pow_le_pow_of_le_one hqBounds.1 hqBounds.2 hk + have hcentral0 : 0 < (1 + α) ^ k := pow_pos (by linarith) _ + have hnormBound : + ‖∑ l ∈ (Finset.univ.erase (0 : ZMod n)), f l‖ ≤ + (n - 1 : ℕ) * q ^ (2 * a * n) * (1 + α) ^ k := by + calc + ‖∑ l ∈ (Finset.univ.erase (0 : ZMod n)), f l‖ ≤ + (n - 1 : ℕ) * (q ^ k * (1 + α) ^ k) := hnormSum + _ = ((n - 1 : ℕ) * q ^ k) * (1 + α) ^ k := by ring + _ ≤ ((n - 1 : ℕ) * q ^ (2 * a * n)) * (1 + α) ^ k := by + apply mul_le_mul_of_nonneg_right _ hcentral0.le + exact mul_le_mul_of_nonneg_left hqPow (by positivity) + _ = (n - 1 : ℕ) * q ^ (2 * a * n) * (1 + α) ^ k := by ring + have herror : + (n - 1 : ℕ) * q ^ (2 * a * n) < + 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) := by + simpa [q, spectralRatio, α, root] using + spectral_error_bound ha hn hpow + have hstrict : + ‖∑ l ∈ (Finset.univ.erase (0 : ZMod n)), f l‖ < + (1 / (16 * (n : ℝ) * (a : ℝ) ^ 2)) * (1 + α) ^ k := + hnormBound.trans_lt (mul_lt_mul_of_pos_right herror hcentral0) + rw [hsum] at hstrict + change + ‖(((n : ℝ) * coeff a n k i * α ^ i - (1 + α) ^ k : ℝ) : ℂ)‖ < + (1 / (16 * (n : ℝ) * (a : ℝ) ^ 2)) * (1 + α) ^ k at hstrict + rw [Complex.norm_real, Real.norm_eq_abs] at hstrict + change + |((n : ℝ) * coeff a n k i * α ^ i) / (1 + α) ^ k - 1| < + 1 / (16 * (n : ℝ) * a ^ 2) + rw [div_sub_one hcentral0.ne', abs_div, abs_of_pos hcentral0, + div_lt_iff₀ hcentral0] + exact hstrict + +private lemma normalized_ratio_close {x y ε : ℝ} + (hε : 0 < ε) (hεsmall : 4 * ε < 1) + (hx : |x - 1| < ε) (hy : |y - 1| < ε) : + |x / y - 1| < 4 * ε ∧ x / y < 2 := by + have hyBounds := abs_lt.mp hy + have hyPos : 0 < y := by nlinarith + have hxy : |x - y| < 2 * ε := by + calc + |x - y| ≤ |x - 1| + |1 - y| := abs_sub_le x 1 y + _ = |x - 1| + |y - 1| := by rw [abs_sub_comm 1 y] + _ < ε + ε := add_lt_add hx hy + _ = 2 * ε := by ring + have hdenLarge : 2 * ε < 4 * ε * y := by + have hyHalf : 1 / 2 < y := by nlinarith + nlinarith [mul_pos (show 0 < 4 * ε by positivity) (sub_pos.mpr hyHalf)] + have hratio : |x / y - 1| < 4 * ε := by + rw [div_sub_one hyPos.ne', abs_div, abs_of_pos hyPos] + exact (div_lt_iff₀ hyPos).2 (hxy.trans hdenLarge) + exact ⟨hratio, by + have := (abs_lt.mp hratio).2 + nlinarith⟩ + +private lemma coeff_ratio_close {a n k i j : ℕ} + (ha : 4 ≤ a) (hn : 1 < n) (hpow : 2 ^ (n - 1) ≤ a) + (hij : i ≤ j) (hj : j < n) (hk : 2 * a * n ≤ k) : + |(coeff a n k i : ℝ) / coeff a n k j - root a n ^ (j - i)| < + root a n ^ (j - i) / (4 * n * a ^ 2) ∧ + (coeff a n k i : ℝ) / coeff a n k j < + 2 * root a n ^ (j - i) := by + let α := root a n + let B := (1 + α) ^ k + let ε := 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) + let si := ((n : ℝ) * coeff a n k i * α ^ i) / B + let sj := ((n : ℝ) * coeff a n k j * α ^ j) / B + have ha0 : 0 < a := by omega + have hα0 : 0 < α := root_pos (n := n) ha0 + have hB0 : 0 < B := pow_pos (by linarith) _ + have hnR : (0 : ℝ) < n := by positivity + have hjk : j ≤ k := by + calc + j ≤ n := hj.le + _ = 1 * n := by simp + _ ≤ (2 * a) * n := Nat.mul_le_mul_right n (by omega) + _ = 2 * a * n := by ring + _ ≤ k := hk + have hcj : 0 < coeff a n k j := coeff_pos_of_lt_of_le hj hjk + have hε : 0 < ε := by dsimp [ε]; positivity + have hεsmall : 4 * ε < 1 := by + dsimp [ε] + rw [show 4 * (1 / (16 * (n : ℝ) * (a : ℝ) ^ 2)) = + 4 / (16 * (n : ℝ) * (a : ℝ) ^ 2) by ring] + apply (div_lt_one (by positivity)).2 + have hn2 : (2 : ℝ) ≤ n := by exact_mod_cast (show 2 ≤ n by omega) + have ha4 : (4 : ℝ) ≤ a := by exact_mod_cast ha + nlinarith [sq_nonneg ((a : ℝ) - 4)] + have hsi : |si - 1| < ε := by + simpa [si, α, B, ε] using + coeff_normalized_close ha hn hpow (by omega : i < n) hk + have hsj : |sj - 1| < ε := by + simpa [sj, α, B, ε] using + coeff_normalized_close ha hn hpow hj hk + have hratio := normalized_ratio_close hε hεsmall hsi hsj + have hpowSplit : α ^ j = α ^ i * α ^ (j - i) := by + rw [← pow_add] + congr 1 + omega + have hrelation : + (coeff a n k i : ℝ) / coeff a n k j = + α ^ (j - i) * (si / sj) := by + dsimp [si, sj] + rw [hpowSplit] + field_simp [hnR.ne', hB0.ne', hα0.ne', + (show (coeff a n k j : ℝ) ≠ 0 by exact_mod_cast hcj.ne')] + change + |(coeff a n k i : ℝ) / coeff a n k j - α ^ (j - i)| < + α ^ (j - i) / (4 * n * a ^ 2) ∧ + (coeff a n k i : ℝ) / coeff a n k j < 2 * α ^ (j - i) + rw [hrelation] + constructor + · rw [show α ^ (j - i) * (si / sj) - α ^ (j - i) = + α ^ (j - i) * (si / sj - 1) by ring, + abs_mul, abs_of_pos (pow_pos hα0 _)] + calc + α ^ (j - i) * |si / sj - 1| < α ^ (j - i) * (4 * ε) := + mul_lt_mul_of_pos_left hratio.1 (pow_pos hα0 _) + _ = α ^ (j - i) / (4 * n * a ^ 2) := by + dsimp [ε] + field_simp + ring + · exact (mul_lt_mul_of_pos_left hratio.2 (pow_pos hα0 _)).trans_eq (by ring) + +private lemma one_add_root_le_three_quarters {a n : ℕ} (ha : 4 ≤ a) (hn : 2 ≤ n) : + 1 + root a n ≤ (3 / 4 : ℝ) * a := by + have hsqrt := Real.sq_sqrt (show (0 : ℝ) ≤ a by positivity) + have hsqrt0 := Real.sqrt_nonneg (a : ℝ) + have haR : (4 : ℝ) ≤ a := by exact_mod_cast ha + have hsqrt_bound : √(a : ℝ) ≤ (a : ℝ) / 2 := by + nlinarith [sq_nonneg (√(a : ℝ) - 2)] + have hroot := root_le_sqrt (show 1 ≤ a by omega) hn + nlinarith + +private lemma mul_three_quarters_pow_four_mul_lt_half {a : ℕ} (ha : 4 ≤ a) : + (a : ℝ) * (3 / 4 : ℝ) ^ (4 * a) < 1 / 2 := by + have ha0 : 0 < a := by omega + have hbase : (3 / 4 : ℝ) ^ 4 < (1 / 2 : ℝ) := by norm_num + have hpow : ((3 / 4 : ℝ) ^ 4) ^ a < ((1 / 2 : ℝ)) ^ a := + pow_lt_pow_left₀ hbase (by positivity) ha0.ne' + have hfour : 4 * a ≤ 2 ^ a := four_mul_le_two_pow ha + have hfourR : (4 : ℝ) * a ≤ (2 : ℝ) ^ a := by exact_mod_cast hfour + have hquarter : (a : ℝ) / 2 ^ a ≤ 1 / 4 := by + rw [div_le_iff₀ (by positivity)] + nlinarith + rw [← pow_mul] at hpow + have hrewrite : (a : ℝ) * (1 / 2 : ℝ) ^ a = (a : ℝ) / 2 ^ a := by + rw [div_pow] + simp [div_eq_mul_inv] + calc + (a : ℝ) * (3 / 4 : ℝ) ^ (4 * a) < + (a : ℝ) * (1 / 2 : ℝ) ^ a := mul_lt_mul_of_pos_left hpow (by positivity) + _ = (a : ℝ) / 2 ^ a := hrewrite + _ ≤ 1 / 4 := hquarter + _ < 1 / 2 := by norm_num + +private lemma reducedEval_lt_modulus {a n k : ℕ} (ha : 4 ≤ a) (hn : 1 < n) + (hk : k ≤ 2 * a * n + 1) : + let K := 2 * a * n + let x := a ^ K + reducedEval a n k x < x ^ n - a := by + let K := 2 * a * n + let x := a ^ K + have ha0 : 0 < a := by omega + have hn0 : 0 < n := by omega + have hK4a : 4 * a ≤ K := by + calc + 4 * a ≤ (2 * n) * a := Nat.mul_le_mul_right a (by omega) + _ = K := by simp [K]; ring + have hK2 : 2 ≤ K := le_trans (by omega : 2 ≤ 4 * a) hK4a + have hx0 : 0 < x := by + exact pow_pos ha0 _ + have hbase0 : (0 : ℝ) ≤ 3 / 4 := by norm_num + have hbase1 : (3 / 4 : ℝ) ≤ 1 := by norm_num + have hbasePow : + (3 / 4 : ℝ) ^ K ≤ (3 / 4 : ℝ) ^ (4 * a) := + pow_le_pow_of_le_one hbase0 hbase1 hK4a + have hnumeric := mul_three_quarters_pow_four_mul_lt_half ha + have hnumericK : + (a : ℝ) * (3 / 4 : ℝ) ^ K < 1 / 2 := by + exact lt_of_le_of_lt + (mul_le_mul_of_nonneg_left hbasePow (by positivity)) hnumeric + have hcoef : 2 * (a : ℝ) * (3 / 4 : ℝ) ^ K < 1 := by + nlinarith + have hrootThree := one_add_root_le_three_quarters ha (by omega : 2 ≤ n) + have hrootA : 1 + root a n ≤ (a : ℝ) := by + calc + 1 + root a n ≤ (3 / 4 : ℝ) * a := hrootThree + _ ≤ a := by nlinarith [show (0 : ℝ) ≤ a by positivity] + have hrootPow : + (1 + root a n) ^ K ≤ ((3 / 4 : ℝ) * a) ^ K := + pow_le_pow_left₀ (by nlinarith [root_pos (n := n) ha0]) hrootThree K + have hleading : 2 * (1 + root a n) ^ (K + 1) < (x : ℝ) := by + calc + 2 * (1 + root a n) ^ (K + 1) = + 2 * (1 + root a n) * (1 + root a n) ^ K := by + rw [pow_succ] + ring + _ ≤ 2 * (a : ℝ) * (((3 / 4 : ℝ) * a) ^ K) := by + apply mul_le_mul + · nlinarith + · exact hrootPow + · exact pow_nonneg (by nlinarith [root_pos (n := n) ha0]) _ + · positivity + _ = (2 * (a : ℝ) * (3 / 4 : ℝ) ^ K) * (a : ℝ) ^ K := by + rw [mul_pow] + ring + _ < 1 * (a : ℝ) ^ K := + mul_lt_mul_of_pos_right hcoef (by positivity) + _ = (x : ℝ) := by simp [x, K] + have hEvalNat := reducedEval_le_top_pow_mul_sum + (a := a) (n := n) (k := k) (x := x) hn0 hx0 + have hEvalCast : + (reducedEval a n k x : ℝ) ≤ + (x : ℝ) ^ (n - 1) * + (∑ i ∈ Finset.range n, coeff a n k i : ℕ) := by + exact_mod_cast hEvalNat + have hCoeff := cast_sum_coeff_le (a := a) (n := n) (k := k) + (by omega : 1 < a) hn0 + have hEval : + (reducedEval a n k x : ℝ) ≤ + (x : ℝ) ^ (n - 1) * (1 + root a n) ^ k := by + exact hEvalCast.trans + (mul_le_mul_of_nonneg_left hCoeff (by positivity)) + have hPowerK : + (1 + root a n) ^ k ≤ (1 + root a n) ^ (K + 1) := by + apply pow_le_pow_right₀ + · nlinarith [root_pos (n := n) ha0] + · simpa [K] using hk + have hdoubleReal : + 2 * (reducedEval a n k x : ℝ) < (x : ℝ) ^ n := by + calc + 2 * (reducedEval a n k x : ℝ) ≤ + 2 * ((x : ℝ) ^ (n - 1) * (1 + root a n) ^ k) := + mul_le_mul_of_nonneg_left hEval (by norm_num) + _ ≤ (x : ℝ) ^ (n - 1) * + (2 * (1 + root a n) ^ (K + 1)) := by + nlinarith [mul_le_mul_of_nonneg_left hPowerK + (show (0 : ℝ) ≤ 2 * (x : ℝ) ^ (n - 1) by positivity)] + _ < (x : ℝ) ^ (n - 1) * x := + mul_lt_mul_of_pos_left hleading (by positivity) + _ = (x : ℝ) ^ n := by + rw [← pow_succ, Nat.sub_add_cancel hn0] + have hdouble : 2 * reducedEval a n k x < x ^ n := by + exact_mod_cast hdoubleReal + have ha2 : 2 * a < a ^ 2 := by nlinarith + have hax : a ^ 2 ≤ x := by + exact Nat.pow_le_pow_right ha0 hK2 + have hxn : x ≤ x ^ n := by + simpa using Nat.pow_le_pow_right hx0 (show 1 ≤ n by omega) + have haSmall : 2 * a < x ^ n := lt_of_lt_of_le ha2 (hax.trans hxn) + change reducedEval a n k x < x ^ n - a + omega + +private lemma root_separation {a n : ℕ} (ha : 2 < a) (hn : 1 < n) + (hpow : 2 ^ (n - 1) ≤ a) (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) : + root a n - n.nthRoot a ≥ root a n / (n * a ^ 2) ∧ + (n.nthRoot a + 1 : ℕ) - root a n ≥ root a n / (n * a ^ 2) := by + let α := root a n + let r := n.nthRoot a + have ha0 : 0 < a := by omega + have hn0 : n ≠ 0 := by omega + have hα0 : 0 < α := root_pos ha0 + have hα1 : 1 < α := one_lt_root (by omega) (by omega) + have hrα : (r : ℝ) < α := nthRoot_lt_root ha0 hn0 hnotpow + have hαr : α < (r : ℝ) + 1 := root_lt_nthRoot_add_one ha0 hn0 + have hr0 : (0 : ℝ) ≤ r := by positivity + have hrootpow : α ^ n = (a : ℝ) := root_pow ha0 hn0 + have hrootpowpred : α * α ^ (n - 1) = (a : ℝ) := by + rw [← pow_succ', Nat.sub_add_cancel (by omega), hrootpow] + have hden : (0 : ℝ) < n * a ^ 2 := by positivity + constructor + · have hltNat : r ^ n < a := by + have hle : r ^ n ≤ a := Nat.pow_nthRoot_le (.inl hn0) + exact lt_of_le_of_ne hle (fun h ↦ hnotpow ⟨r, h⟩) + have hgapNat : 1 ≤ a - r ^ n := by omega + have hgap : (1 : ℝ) ≤ α ^ n - (r : ℝ) ^ n := by + have hcast : (1 : ℝ) ≤ ((a - r ^ n : ℕ) : ℝ) := by exact_mod_cast hgapNat + rw [Nat.cast_sub hltNat.le, Nat.cast_pow] at hcast + simpa [hrootpow] using hcast + have habs := abs_pow_sub_pow_le (a := α) (b := (r : ℝ)) n + have hpowdiff : 0 ≤ α ^ n - (r : ℝ) ^ n := sub_nonneg.mpr <| by + exact pow_le_pow_left₀ hr0 hrα.le n + rw [abs_of_nonneg hpowdiff, abs_of_nonneg hα0.le, abs_of_nonneg hr0, + max_eq_left hrα.le, abs_of_nonneg (sub_nonneg.mpr hrα.le)] at habs + have hone : (1 : ℝ) ≤ (α - r) * n * α ^ (n - 1) := hgap.trans habs + have hαB : α * α ^ (n - 1) ≤ (a : ℝ) ^ 2 := by + rw [hrootpowpred] + exact_mod_cast (show a ≤ a ^ 2 by nlinarith) + have hmul : α ≤ (α - r) * n * (a : ℝ) ^ 2 := by + calc + α = α * 1 := by ring + _ ≤ α * ((α - r) * n * α ^ (n - 1)) := + mul_le_mul_of_nonneg_left hone hα0.le + _ = ((α - r) * n) * (α * α ^ (n - 1)) := by ring + _ ≤ ((α - r) * n) * (a : ℝ) ^ 2 := + mul_le_mul_of_nonneg_left hαB (mul_nonneg (sub_nonneg.mpr hrα.le) (by positivity)) + rw [ge_iff_le, div_le_iff₀ hden] + simpa [mul_assoc, mul_left_comm, mul_comm] using hmul + · have hgapNat : 1 ≤ (r + 1) ^ n - a := by + have hlt : a < (r + 1) ^ n := by simpa [r] using Nat.lt_pow_nthRoot_add_one hn0 a + omega + have hgap : (1 : ℝ) ≤ ((r : ℝ) + 1) ^ n - α ^ n := by + have hlt : a ≤ (r + 1) ^ n := by + simpa [r] using (Nat.lt_pow_nthRoot_add_one hn0 a).le + have hcast : (1 : ℝ) ≤ ((((r + 1) ^ n - a : ℕ)) : ℝ) := by exact_mod_cast hgapNat + rw [Nat.cast_sub hlt, Nat.cast_pow, Nat.cast_add, Nat.cast_one] at hcast + simpa [hrootpow] using hcast + have habs := abs_pow_sub_pow_le (a := (r : ℝ) + 1) (b := α) n + have hpowdiff : 0 ≤ ((r : ℝ) + 1) ^ n - α ^ n := sub_nonneg.mpr <| by + exact pow_le_pow_left₀ hα0.le hαr.le n + rw [abs_of_nonneg hpowdiff, abs_of_nonneg (by positivity : (0 : ℝ) ≤ r + 1), + abs_of_nonneg hα0.le, max_eq_left hαr.le, + abs_of_nonneg (sub_nonneg.mpr hαr.le)] at habs + have hone : (1 : ℝ) ≤ ((r : ℝ) + 1 - α) * n * ((r : ℝ) + 1) ^ (n - 1) := + hgap.trans habs + have hr_two : (r : ℝ) + 1 ≤ 2 * α := by linarith + have hαB : α * ((r : ℝ) + 1) ^ (n - 1) ≤ (a : ℝ) ^ 2 := by + calc + α * ((r : ℝ) + 1) ^ (n - 1) ≤ α * (2 * α) ^ (n - 1) := by gcongr + _ = (2 : ℝ) ^ (n - 1) * (α * α ^ (n - 1)) := by + rw [mul_pow] + ring + _ = (2 : ℝ) ^ (n - 1) * a := by rw [hrootpowpred] + _ ≤ (a : ℝ) * a := by gcongr; exact_mod_cast hpow + _ = (a : ℝ) ^ 2 := by ring + have hmul : α ≤ ((r : ℝ) + 1 - α) * n * (a : ℝ) ^ 2 := by + calc + α = α * 1 := by ring + _ ≤ α * (((r : ℝ) + 1 - α) * n * ((r : ℝ) + 1) ^ (n - 1)) := + mul_le_mul_of_nonneg_left hone hα0.le + _ = (((r : ℝ) + 1 - α) * n) * (α * ((r : ℝ) + 1) ^ (n - 1)) := by + ring + _ ≤ (((r : ℝ) + 1 - α) * n) * (a : ℝ) ^ 2 := + mul_le_mul_of_nonneg_left hαB (mul_nonneg (sub_nonneg.mpr hαr.le) (by positivity)) + rw [ge_iff_le, div_le_iff₀ hden] + push_cast + simpa [mul_assoc, mul_left_comm, mul_comm] using hmul + +private lemma div_sub_one_eq_nthRoot_of_approx {a n N D : ℕ} + (ha : 2 < a) (hn : 1 < n) (hpow : 2 ^ (n - 1) ≤ a) + (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) + (happrox : + |(N : ℝ) / (D : ℝ) - 1 - root a n| < + root a n / (2 * n * a ^ 2)) : + N / D - 1 = n.nthRoot a := by + have hsep := root_separation ha hn hpow hnotpow + have hα0 : 0 < root a n := root_pos (by omega) + have hhalf : + root a n / (2 * n * a ^ 2) < root a n / (n * a ^ 2) := by + apply div_lt_div_of_pos_left hα0 + · positivity + · nlinarith [show (0 : ℝ) < n * a ^ 2 by positivity] + have habs := abs_lt.mp happrox + have hlo : (n.nthRoot a : ℝ) < (N : ℝ) / (D : ℝ) - 1 := by + have := hsep.1 + linarith + have hhi : (N : ℝ) / (D : ℝ) - 1 < (n.nthRoot a : ℝ) + 1 := by + have := hsep.2 + push_cast at this + linarith + have hf : ⌊(N : ℝ) / (D : ℝ)⌋₊ = n.nthRoot a + 1 := + Nat.floor_eq_on_Ico (n.nthRoot a + 1) _ + ⟨by push_cast; linarith, by push_cast; linarith⟩ + rw [Nat.floor_div_eq_div] at hf + omega + +private lemma shunia_integer_root_three_two : + let k := 2 * 3 * 2 + let x := 3 ^ k + let m := x ^ 2 - 3 + Nat.nthRoot 2 3 = + ((x + 1) ^ (k + 1) % m) / ((x + 1) ^ k % m) - 1 := by + have hroot : Nat.nthRoot 2 3 = 1 := by decide + rw [hroot] + norm_num [Nat.pow_mod] + +private lemma shunia_integer_root_of_four_le + (a n : ℕ) (ha : 4 ≤ a) (hn : 1 < n) + (hlog : n ≤ Nat.log2 a + 1) + (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) : + let k := 2 * a * n + let x := a ^ k + let m := x ^ n - a + n.nthRoot a = + ((x + 1) ^ (k + 1) % m) / ((x + 1) ^ k % m) - 1 := by + let K := 2 * a * n + let X := a ^ K + let M := X ^ n - a + let U := coeff a n K (n - 1) + let V := coeff a n K (n - 2) + let C := coeff a n (K + 1) (n - 1) + let D := reducedEval a n K X + let N := reducedEval a n (K + 1) X + change n.nthRoot a = ((X + 1) ^ (K + 1) % M) / ((X + 1) ^ K % M) - 1 + have ha0 : 0 < a := by omega + have hn0 : 0 < n := by omega + have hpow : 2 ^ (n - 1) ≤ a := by + rw [← Nat.le_log2 ha0.ne'] + omega + have hna : n ≤ a := by + have := (n - 1).lt_two_pow_self + omega + have hKtop : n - 1 ≤ K := by + calc + n - 1 ≤ n := Nat.sub_le n 1 + _ = 1 * n := by simp + _ ≤ (2 * a) * n := Nat.mul_le_mul_right n (by omega) + _ = K := by simp [K] + have hKpos : 1 ≤ K := by + dsimp [K] + nlinarith + have hX0 : 0 < X := by simp [X, ha0] + have haX : a ≤ X := by + dsimp [X] + simpa using Nat.pow_le_pow_right ha0 hKpos + have hXXn : X ≤ X ^ n := by + simpa using Nat.pow_le_pow_right hX0 (show 1 ≤ n by omega) + have haXn : a ≤ X ^ n := haX.trans hXXn + have hsmallK : reducedEval a n K X < M := by + simpa [K, X, M] using + (reducedEval_lt_modulus (a := a) (n := n) (k := 2 * a * n) + ha hn (by omega)) + have hsmallSucc : reducedEval a n (K + 1) X < M := by + simpa [K, X, M] using + (reducedEval_lt_modulus (a := a) (n := n) (k := 2 * a * n + 1) + ha hn (by omega)) + have hresK : (X + 1) ^ K % M = D := by + simpa [D, M] using + add_one_pow_mod_eq_reducedEval (a := a) (n := n) (k := K) (x := X) + hn0 haXn hsmallK + have hresSucc : (X + 1) ^ (K + 1) % M = N := by + simpa [N, M] using + add_one_pow_mod_eq_reducedEval (a := a) (n := n) (k := K + 1) (x := X) + hn0 haXn hsmallSucc + have hU : 0 < U := by + exact coeff_pos_of_lt_of_le (by omega) hKtop + have hC : 0 < C := by + exact coeff_pos_of_lt_of_le (by omega) (by omega) + have hα : 1 < root a n := one_lt_root (by omega) hn0 + have hαpow : root a n ^ n = (a : ℝ) := root_pow ha0 (by omega) + have hrelK : ∀ i < n - 1, + (coeff a n K i : ℝ) / coeff a n K (n - 1) < + 2 * root a n ^ (n - 1 - i) := by + intro i hi + exact (coeff_ratio_close ha hn hpow (by omega) (by omega) (by simp [K])).2 + have hrelSucc : ∀ i < n - 1, + (coeff a n (K + 1) i : ℝ) / coeff a n (K + 1) (n - 1) < + 2 * root a n ^ (n - 1 - i) := by + intro i hi + exact (coeff_ratio_close ha hn hpow (by omega) (by omega) (by simp [K])).2 + have hcoeff : + |(V : ℝ) / U - root a n| < root a n / (4 * n * a ^ 2) := by + simpa [U, V, show n - 1 - (n - 2) = 1 by omega] using + (coeff_ratio_close (a := a) (n := n) (k := K) (i := n - 2) (j := n - 1) + ha hn hpow (by omega) (by omega) (by simp [K])).1 + have hrec : C = U + V := by + simpa [C, U, V] using coeff_succ_top (a := a) (n := n) (k := K) hn + have hCUeq : (C : ℝ) / U = 1 + (V : ℝ) / U := by + rw [hrec] + push_cast + field_simp [show (U : ℝ) ≠ 0 by exact_mod_cast hU.ne'] + have herrorOne : root a n / (4 * n * a ^ 2) < 1 := by + apply (div_lt_one (by positivity)).2 + have hrootA := root_le_nat (a := a) (n := n) (by omega) hn0 + have hlarge : (a : ℝ) < 4 * n * (a : ℝ) ^ 2 := by + have hfactor : (1 : ℝ) < 4 * n * a := by + have hn2 : (2 : ℝ) ≤ n := by exact_mod_cast (show 2 ≤ n by omega) + have ha4 : (4 : ℝ) ≤ a := by exact_mod_cast ha + nlinarith + nlinarith [mul_pos (show (0 : ℝ) < a by positivity) + (sub_pos.mpr hfactor)] + exact hrootA.trans_lt hlarge + have hCU : (C : ℝ) / U < 2 * a := by + have hVU : (V : ℝ) / U < root a n + 1 := by + have := (abs_lt.mp hcoeff).2 + linarith + rw [hCUeq] + have hrootA := root_le_nat (a := a) (n := n) (by omega) hn0 + have haR : (4 : ℝ) ≤ a := by exact_mod_cast ha + nlinarith + have heval : + |(N : ℝ) / D - (C : ℝ) / U| < root a n / (4 * n * a ^ 2) := by + simpa [N, D, C, U, reducedEval, X, K] using + (eval_ratio_close_leading_ratio + (α := root a n) + (fun i ↦ coeff a n K i) + (fun i ↦ coeff a n (K + 1) i) + ha hn hna hα hαpow hU hC hrelK hrelSucc hCU) + have htotal : + |(N : ℝ) / D - 1 - root a n| < + root a n / (2 * n * a ^ 2) := by + calc + |(N : ℝ) / D - 1 - root a n| = + |((N : ℝ) / D - (C : ℝ) / U) + + ((V : ℝ) / U - root a n)| := by + rw [hCUeq] + congr 1 + ring + _ ≤ |(N : ℝ) / D - (C : ℝ) / U| + + |(V : ℝ) / U - root a n| := abs_add_le _ _ + _ < root a n / (4 * n * a ^ 2) + + root a n / (4 * n * a ^ 2) := add_lt_add heval hcoeff + _ = root a n / (2 * n * a ^ 2) := by ring + have hrootResult := + div_sub_one_eq_nthRoot_of_approx + (a := a) (n := n) (N := N) (D := D) + (by omega) hn hpow hnotpow htotal + rw [hresSucc, hresK] + exact hrootResult.symm + +/-- Shunia's integer-root formula, formerly Conjecture 6.1. -/ +theorem shunia_integer_root + (a n : ℕ) (ha : 2 < a) (hn : 1 < n) + (hlog : n ≤ Nat.log2 a + 1) + (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) : + let k := 2 * a * n + let x := a ^ k + let m := x ^ n - a + n.nthRoot a = + ((x + 1) ^ (k + 1) % m) / ((x + 1) ^ k % m) - 1 := by + by_cases ha4 : 4 ≤ a + · exact shunia_integer_root_of_four_le a n ha4 hn hlog hnotpow + · have ha3 : a = 3 := by omega + subst a + have hn2 : n = 2 := by + have hlog3 : Nat.log2 3 = 1 := by decide + rw [hlog3] at hlog + omega + subst n + exact shunia_integer_root_three_two + +end ShuniaIntegerRoot diff --git a/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean b/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean new file mode 100644 index 00000000000000..f87a9d5c336764 --- /dev/null +++ b/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean @@ -0,0 +1,543 @@ +/- +Copyright (c) 2026 Ravi Bajaj and Ben Burns. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ravi Bajaj, Ben Burns +-/ +module + +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.Convex.SpecificFunctions.Deriv + +/-! +# Quantitative estimates for Shunia's integer-root formula + +This file proves the uniform spectral estimate used in the proof of Shunia's integer-root +formula. If `α = a ^ (1 / n)` and + +`q = sqrt (1 + α ^ 2 + 2 * α * cos (2 * π / n)) / (1 + α)`, + +then, under the admissibility hypotheses, `(n - 1) * q ^ (2 * a * n)` is smaller than +`1 / (16 * n * a ^ 2)`. +-/ + +@[expose] public section + +open Real + +namespace ShuniaIntegerRoot + +private lemma nat_le_two_pow_pred {n : ℕ} (hn : 1 ≤ n) : n ≤ 2 ^ (n - 1) := by + have h := (n - 1).lt_two_pow_self + omega + +private lemma nat_sq_le_two_pow {n : ℕ} (hn : 4 ≤ n) : n ^ 2 ≤ 2 ^ n := by + induction n, hn using Nat.le_induction with + | base => norm_num + | succ n hn ih => + calc + (n + 1) ^ 2 ≤ 2 * n ^ 2 := by nlinarith + _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 ih + _ = 2 ^ (n + 1) := by rw [pow_succ]; ring + +private lemma baseline_target_le_two_pow {n : ℕ} (hn : 1 ≤ n) : + 16 * n * (n - 1) * (2 ^ (n - 1)) ^ 2 ≤ 2 ^ (4 * n) := by + have h₁ := nat_le_two_pow_pred hn + have h₂ : n - 1 ≤ 2 ^ (n - 1) := (Nat.sub_le n 1).trans h₁ + calc + 16 * n * (n - 1) * (2 ^ (n - 1)) ^ 2 + ≤ 16 * (2 ^ (n - 1)) * (2 ^ (n - 1)) * (2 ^ (n - 1)) ^ 2 := by + gcongr + _ = 2 ^ (4 * n) := by + rw [show 16 = 2 ^ 4 by norm_num] + simp only [← pow_add, ← pow_mul] + congr 1 + omega + +private lemma log_two_lt_three_four : Real.log 2 < (3 : ℝ) / 4 := by + rw [Real.log_lt_iff_lt_exp (by norm_num)] + have h := Real.sum_le_exp_of_nonneg (x := (3 : ℝ) / 4) (by norm_num) 3 + norm_num [Finset.sum_range_succ] at h ⊢ + exact lt_of_lt_of_le (by norm_num) h + +private lemma eight_thirds_lt_exp_one : (8 : ℝ) / 3 < Real.exp 1 := by + have h := Real.sum_le_exp_of_nonneg (x := (1 : ℝ)) (by norm_num) 5 + norm_num [Finset.sum_range_succ] at h ⊢ + exact lt_of_lt_of_le (by norm_num) h + +private lemma exp_neg_lt_inv {T P : ℝ} (hT : 0 < T) (hlog : Real.log T < P) : + Real.exp (-P) < 1 / T := by + calc + Real.exp (-P) < Real.exp (-Real.log T) := Real.exp_lt_exp.mpr (neg_lt_neg hlog) + _ = 1 / T := by rw [Real.exp_neg, Real.exp_log hT]; simp [one_div] + +private lemma baseline_exponent_bound {n : ℕ} (hn : 3 ≤ n) : + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) < + 6 * (2 : ℝ) ^ (n - 1) / n := by + rcases eq_or_lt_of_le hn with rfl | hn4 + · norm_num only [Nat.cast_ofNat, Nat.cast_sub (by omega), Nat.cast_one, + Nat.reduceSubDiff, Nat.reducePow, Nat.cast_pow] + rw [Real.log_lt_iff_lt_exp (by norm_num)] + have he : (8 / 3 : ℝ) < Real.exp 1 := eight_thirds_lt_exp_one + have hp : (8 / 3 : ℝ) ^ 8 < (Real.exp 1) ^ 8 := by + exact pow_lt_pow_left₀ he (by positivity) (by norm_num) + have hp' : (8 / 3 : ℝ) ^ 8 < Real.exp 8 := by + calc + _ < (Real.exp 1) ^ 8 := hp + _ = Real.exp 8 := by rw [← Real.exp_nat_mul]; norm_num + exact (by norm_num : (1536 : ℝ) < (8 / 3) ^ 8).trans hp' + · have hn4' : 4 ≤ n := by omega + have htarget_nat := baseline_target_le_two_pow (show 1 ≤ n by omega) + have htarget : + (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) ≤ + (2 : ℝ) ^ (4 * n) := by + exact_mod_cast htarget_nat + have hpos : + 0 < 16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2 := by + have hnpos : (0 : ℝ) < n := by positivity + have hn1pos : (0 : ℝ) < (n - 1 : ℕ) := by + exact_mod_cast (show 0 < n - 1 by omega) + positivity + have hlog : + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) ≤ + (4 * n : ℝ) * Real.log 2 := by + calc + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) + ≤ Real.log ((2 : ℝ) ^ (4 * n)) := Real.log_le_log hpos htarget + _ = (4 * n : ℕ) * Real.log 2 := Real.log_pow 2 (4 * n) + _ = (4 * n : ℝ) * Real.log 2 := by norm_num + have hlog3 : + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) < + 3 * n := by + calc + _ ≤ (4 * n : ℝ) * Real.log 2 := hlog + _ < (4 * n : ℝ) * ((3 : ℝ) / 4) := + mul_lt_mul_of_pos_left log_two_lt_three_four (by positivity) + _ = 3 * n := by ring + have hsquare := nat_sq_le_two_pow hn4' + have hsquare' : (n : ℝ) ^ 2 ≤ (2 : ℝ) ^ n := by exact_mod_cast hsquare + have hL : (3 : ℝ) * n ≤ 6 * (2 : ℝ) ^ (n - 1) / n := by + rw [le_div_iff₀ (by positivity : (0 : ℝ) < n)] + have hp : (2 : ℝ) ^ n = 2 * (2 : ℝ) ^ (n - 1) := by + calc + (2 : ℝ) ^ n = 2 ^ ((n - 1) + 1) := by + congr 1 + omega + _ = 2 ^ (n - 1) * 2 := by rw [pow_succ] + _ = 2 * 2 ^ (n - 1) := by ring + calc + 3 * (n : ℝ) * n = 3 * (n : ℝ) ^ 2 := by ring + _ ≤ 3 * (2 : ℝ) ^ n := by gcongr + _ = 6 * (2 : ℝ) ^ (n - 1) := by rw [hp]; ring + exact hlog3.trans_le hL + +private lemma two_ninths_le_root_factor {x : ℝ} (hx₁ : 1 ≤ x) (hx₂ : x ≤ 2) : + (2 : ℝ) / 9 ≤ x / (1 + x) ^ 2 := by + rw [div_le_div_iff₀ (by norm_num : (0 : ℝ) < 9) (sq_pos_of_pos (by linarith))] + have hprod : 0 ≤ (2 * x - 1) * (2 - x) := + mul_nonneg (by linarith) (by linarith) + nlinarith + +private lemma four_ninths_div_le_root_factor {x : ℝ} (hx : 2 ≤ x) : + (4 : ℝ) / (9 * x) ≤ x / (1 + x) ^ 2 := by + rw [div_le_div_iff₀ (mul_pos (by norm_num) (by linarith)) + (sq_pos_of_pos (by linarith))] + have hprod : 0 ≤ (x - 2) * (5 * x + 2) := + mul_nonneg (by linarith) (by linarith) + nlinarith + +private lemma exponent_gt_log_of_pow {a n : ℕ} {α : ℝ} + (hn : 3 ≤ n) (ha₀ : 2 ^ (n - 1) ≤ a) + (hα₁ : 1 ≤ α) (hαpow : α ^ n = (a : ℝ)) : + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) < + 27 * (a : ℝ) * α / ((n : ℝ) * (1 + α) ^ 2) := by + let A : ℝ := (2 : ℝ) ^ (n - 1) + let L : ℝ := 6 * A / n + let R : ℝ := Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2) + have hApos : 0 < A := by dsimp [A]; positivity + have hnpos : (0 : ℝ) < n := by positivity + have hn1pos : (0 : ℝ) < (n - 1 : ℕ) := by + exact_mod_cast (show 0 < n - 1 by omega) + have haNat : 0 < a := lt_of_lt_of_le (by positivity : 0 < 2 ^ (n - 1)) ha₀ + have hapos : (0 : ℝ) < a := by exact_mod_cast haNat + have hαpos : 0 < α := lt_of_lt_of_le zero_lt_one hα₁ + have hR_L : R < L := by + simpa only [A, L, R] using baseline_exponent_bound hn + have hnA := nat_le_two_pow_pred (show 1 ≤ n by omega) + have hnA' : (n : ℝ) ≤ A := by + dsimp [A] + exact_mod_cast hnA + have hL6 : 6 ≤ L := by + dsimp [L] + rw [le_div_iff₀ hnpos] + nlinarith + have hLpos : 0 < L := lt_of_lt_of_le (by norm_num) hL6 + rcases le_total α 2 with hα₂ | hα₂ + · let s : ℝ := (a : ℝ) / A + have hspos : 0 < s := div_pos hapos hApos + have hs₁ : 1 ≤ s := by + dsimp [s] + rw [le_div_iff₀ hApos] + dsimp [A] + simpa using (show ((2 : ℝ) ^ (n - 1) ≤ (a : ℝ)) by exact_mod_cast ha₀) + have ha_eq : (a : ℝ) = A * s := by + dsimp [s] + field_simp + have hlog_eq : + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) = + R + 2 * Real.log s := by + rw [ha_eq] + have hbase_ne : + 16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2 ≠ 0 := by positivity + calc + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (A * s) ^ 2) + = Real.log ((16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2) * s ^ 2) := by + congr 1 + ring + _ = Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2) + + Real.log (s ^ 2) := Real.log_mul hbase_ne (pow_ne_zero 2 hspos.ne') + _ = R + 2 * Real.log s := by rw [Real.log_pow]; simp [R] + have hlogs : Real.log s ≤ s - 1 := Real.log_le_sub_one_of_pos hspos + have hsmall : R + 2 * Real.log s < L * s := by + have hmul : 2 * (s - 1) ≤ L * (s - 1) := + mul_le_mul_of_nonneg_right (by linarith : (2 : ℝ) ≤ L) (sub_nonneg.mpr hs₁) + nlinarith + have hfac := two_ninths_le_root_factor hα₁ hα₂ + have hP : + 6 * (a : ℝ) / n ≤ + 27 * (a : ℝ) * α / ((n : ℝ) * (1 + α) ^ 2) := by + calc + 6 * (a : ℝ) / n = + (27 * (a : ℝ) / n) * ((2 : ℝ) / 9) := by ring + _ ≤ (27 * (a : ℝ) / n) * (α / (1 + α) ^ 2) := by + gcongr + _ = 27 * (a : ℝ) * α / ((n : ℝ) * (1 + α) ^ 2) := by + field_simp + rw [hlog_eq] + exact hsmall.trans_le <| by + calc + L * s = 6 * (a : ℝ) / n := by rw [ha_eq]; simp [L]; ring + _ ≤ _ := hP + · let t : ℝ := α / 2 + have htpos : 0 < t := div_pos hαpos (by norm_num) + have ht₁ : 1 ≤ t := by dsimp [t]; linarith + have hα_eq : α = 2 * t := by dsimp [t]; ring + have ha_eq : (a : ℝ) = A * (2 * t ^ n) := by + rw [← hαpow, hα_eq] + dsimp [A] + rw [mul_pow] + have htwo : (2 : ℝ) ^ n = 2 * 2 ^ (n - 1) := by + calc + (2 : ℝ) ^ n = 2 ^ ((n - 1) + 1) := by + congr 1 + omega + _ = 2 ^ (n - 1) * 2 := by rw [pow_succ] + _ = 2 * 2 ^ (n - 1) := by ring + rw [htwo] + ring + have hlog_eq : + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) = + R + 2 * Real.log 2 + 2 * n * Real.log t := by + rw [ha_eq] + have hbase_ne : + 16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2 ≠ 0 := by positivity + calc + Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (A * (2 * t ^ n)) ^ 2) + = Real.log ((16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2) * + (2 * t ^ n) ^ 2) := by + congr 1 + ring + _ = Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2) + + Real.log ((2 * t ^ n) ^ 2) := + Real.log_mul hbase_ne + (pow_ne_zero 2 (mul_ne_zero (by norm_num) (pow_ne_zero _ htpos.ne'))) + _ = R + 2 * Real.log 2 + 2 * n * Real.log t := by + rw [Real.log_pow, Real.log_mul (by norm_num) (pow_ne_zero _ htpos.ne'), + Real.log_pow] + simp [R] + ring + have hlogt : Real.log t ≤ t - 1 := Real.log_le_sub_one_of_pos htpos + have htpow : 1 + (n - 1 : ℕ) * (t - 1) ≤ t ^ (n - 1) := by + simpa [add_sub_cancel_left] using + (one_add_mul_le_pow (show (-2 : ℝ) ≤ t - 1 by linarith) (n - 1)) + have hsecond : 2 * Real.log 2 + 2 * n * Real.log t ≤ L * t ^ (n - 1) := by + have hcoef : (2 : ℝ) * n ≤ 6 * (↑(n - 1) : ℝ) := by + norm_cast + omega + have hlinear : + (3 : ℝ) / 2 + 2 * n * (t - 1) ≤ + 6 * (1 + (n - 1 : ℕ) * (t - 1)) := by + have hmul := mul_le_mul_of_nonneg_right hcoef (sub_nonneg.mpr ht₁) + nlinarith + calc + 2 * Real.log 2 + 2 * n * Real.log t + ≤ (3 : ℝ) / 2 + 2 * n * (t - 1) := by + nlinarith [log_two_lt_three_four.le] + _ ≤ 6 * (1 + (n - 1 : ℕ) * (t - 1)) := hlinear + _ ≤ 6 * t ^ (n - 1) := by gcongr + _ ≤ L * t ^ (n - 1) := by gcongr + have ht_pow_one : 1 ≤ t ^ (n - 1) := one_le_pow₀ ht₁ + have htotal : + R + 2 * Real.log 2 + 2 * n * Real.log t < + 2 * L * t ^ (n - 1) := by + have hfirst : R < L * t ^ (n - 1) := + hR_L.trans_le (by simpa using mul_le_mul_of_nonneg_left ht_pow_one hLpos.le) + nlinarith + have hfac := four_ninths_div_le_root_factor hα₂ + have hP : + 12 * (a : ℝ) / ((n : ℝ) * α) ≤ + 27 * (a : ℝ) * α / ((n : ℝ) * (1 + α) ^ 2) := by + calc + 12 * (a : ℝ) / ((n : ℝ) * α) = + (27 * (a : ℝ) / n) * ((4 : ℝ) / (9 * α)) := by ring + _ ≤ (27 * (a : ℝ) / n) * (α / (1 + α) ^ 2) := by gcongr + _ = 27 * (a : ℝ) * α / ((n : ℝ) * (1 + α) ^ 2) := by + field_simp + have hlower : + 2 * L * t ^ (n - 1) = 12 * (a : ℝ) / ((n : ℝ) * α) := by + rw [ha_eq, hα_eq] + dsimp [L] + rw [show t ^ n = t ^ (n - 1) * t by + conv_lhs => rw [show n = (n - 1) + 1 by omega, pow_succ]] + field_simp + ring + rw [hlog_eq] + exact htotal.trans_le (hlower.le.trans hP) + +private lemma sin_pi_div_lower {n : ℕ} (hn : 3 ≤ n) : + (3 * Real.sqrt 3) / (2 * n) ≤ Real.sin (Real.pi / n) := by + have hlam0 : (0 : ℝ) ≤ 3 / n := by positivity + have hlam1 : (3 : ℝ) / n ≤ 1 := by + rw [div_le_one (by positivity : (0 : ℝ) < n)] + exact_mod_cast hn + have hpi3 : Real.pi / 3 ∈ Set.Icc (0 : ℝ) Real.pi := by + constructor + · positivity + · nlinarith [Real.pi_pos] + have hc := strictConcaveOn_sin_Icc.concaveOn.2 + (show (0 : ℝ) ∈ Set.Icc (0 : ℝ) Real.pi by simp [Real.pi_pos.le]) + hpi3 (sub_nonneg.mpr hlam1) hlam0 + calc + (3 * Real.sqrt 3) / (2 * n) = (3 / n) * (Real.sqrt 3 / 2) := by ring + _ ≤ Real.sin (Real.pi / n) := by + simpa [Real.sin_pi_div_three, smul_eq_mul] using hc + +private lemma one_sub_cos_two_pi_div_lower {n : ℕ} (hn : 3 ≤ n) : + (27 : ℝ) / (2 * n ^ 2) ≤ 1 - Real.cos (2 * Real.pi / n) := by + have hsin := sin_pi_div_lower hn + have hlower_nonneg : (0 : ℝ) ≤ (3 * Real.sqrt 3) / (2 * n) := by positivity + have hsin_sq : + ((3 * Real.sqrt 3) / (2 * n)) ^ 2 ≤ (Real.sin (Real.pi / n)) ^ 2 := + pow_le_pow_left₀ hlower_nonneg hsin 2 + have hsqrt : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num) + have htrig : + 1 - Real.cos (2 * Real.pi / n) = 2 * (Real.sin (Real.pi / n)) ^ 2 := by + rw [show 2 * Real.pi / (n : ℝ) = 2 * (Real.pi / n) by ring, + Real.sin_sq_eq_half_sub] + ring + rw [htrig] + rw [div_pow] at hsin_sq + have hn0 : (n : ℝ) ≠ 0 := by positivity + field_simp [hn0] at hsin_sq ⊢ + nlinarith [hsqrt] + +private lemma spectral_error_bound_n_ge_three {a n : ℕ} (hn : 3 ≤ n) + (ha₀ : 2 ^ (n - 1) ≤ a) : + let α : ℝ := (a : ℝ) ^ ((n : ℝ)⁻¹) + let q : ℝ := + Real.sqrt (1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / n)) / (1 + α) + (n - 1 : ℕ) * q ^ (2 * a * n) < + 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) := by + let α : ℝ := (a : ℝ) ^ ((n : ℝ)⁻¹) + let c : ℝ := Real.cos (2 * Real.pi / n) + let rad : ℝ := 1 + α ^ 2 + 2 * α * c + let q : ℝ := Real.sqrt rad / (1 + α) + let D : ℝ := (1 + α) ^ 2 + let u : ℝ := 2 * α * (1 - c) / D + let v : ℝ := 27 * α / ((n : ℝ) ^ 2 * D) + let P : ℝ := 27 * (a : ℝ) * α / ((n : ℝ) * D) + have hapos : (0 : ℝ) < a := by + exact_mod_cast lt_of_lt_of_le (by positivity : 0 < 2 ^ (n - 1)) ha₀ + have hα₁ : 1 ≤ α := by + dsimp [α] + apply Real.one_le_rpow + · exact_mod_cast (show 1 ≤ n by omega).trans + ((nat_le_two_pow_pred (show 1 ≤ n by omega)).trans ha₀) + · positivity + have hαpos : 0 < α := lt_of_lt_of_le zero_lt_one hα₁ + have hnpos : (0 : ℝ) < n := by positivity + have hDpos : 0 < D := by dsimp [D]; positivity + have hrad : 0 ≤ rad := by + have hc := Real.neg_one_le_cos (2 * Real.pi / (n : ℝ)) + dsimp [rad, c] + nlinarith [sq_nonneg (α - 1)] + have hq_sq : q ^ 2 = rad / D := by + dsimp [q, D] + rw [div_pow, Real.sq_sqrt hrad] + have hratio : rad / D = 1 - u := by + dsimp [rad, D, u] + field_simp + ring + have hcos : + (27 : ℝ) / (2 * n ^ 2) ≤ 1 - c := by + simpa only [c] using one_sub_cos_two_pi_div_lower hn + have huv : v ≤ u := by + calc + v = (2 * α / D) * ((27 : ℝ) / (2 * n ^ 2)) := by + dsimp [v] + field_simp + _ ≤ (2 * α / D) * (1 - c) := by + exact mul_le_mul_of_nonneg_left hcos (by positivity) + _ = u := by dsimp [u]; ring + have hq_sq_exp : q ^ 2 ≤ Real.exp (-v) := by + rw [hq_sq, hratio] + exact (Real.one_sub_le_exp_neg u).trans (Real.exp_le_exp.mpr (neg_le_neg huv)) + have hpow_exp : q ^ (2 * a * n) ≤ Real.exp (-P) := by + have hpowers : + (q ^ 2) ^ (a * n) ≤ (Real.exp (-v)) ^ (a * n) := + pow_le_pow_left₀ (sq_nonneg q) hq_sq_exp (a * n) + have hexponent : (2 * a * n : ℕ) = 2 * (a * n) := by simp [mul_assoc] + calc + q ^ (2 * a * n) = (q ^ 2) ^ (a * n) := by + rw [hexponent, pow_mul] + _ ≤ (Real.exp (-v)) ^ (a * n) := hpowers + _ = Real.exp ((a * n : ℕ) * (-v)) := by + rw [Real.exp_nat_mul] + _ = Real.exp (-P) := by + congr 1 + dsimp [v, P] + push_cast + field_simp + have hexp : Real.exp (-P) < + 1 / (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) := by + apply exp_neg_lt_inv + · have : 0 < n - 1 := by omega + positivity + · simpa only [P, D, α] using + exponent_gt_log_of_pow hn ha₀ hα₁ + (Real.rpow_inv_natCast_pow (by positivity) (by omega)) + have hq : q ^ (2 * a * n) < + 1 / (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) := by + exact hpow_exp.trans_lt hexp + have hn1pos : (0 : ℝ) < (n - 1 : ℕ) := by + exact_mod_cast (show 0 < n - 1 by omega) + have hmul := mul_lt_mul_of_pos_left hq hn1pos + change (↑(n - 1) : ℝ) * q ^ (2 * a * n) < 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) + calc + (↑(n - 1) : ℝ) * q ^ (2 * a * n) + < (↑(n - 1) : ℝ) * + (1 / (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2)) := hmul + _ = 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) := by + field_simp + +private lemma exponent_two_gt_log {a : ℕ} (ha : 4 ≤ a) : + let α : ℝ := (a : ℝ) ^ ((2 : ℝ)⁻¹) + Real.log (32 * (a : ℝ) ^ 2) < + 8 * (a : ℝ) * α / (1 + α) ^ 2 := by + let α : ℝ := (a : ℝ) ^ ((2 : ℝ)⁻¹) + let t : ℝ := α / 2 + have hαpow : α ^ 2 = (a : ℝ) := by + exact Real.rpow_inv_natCast_pow (by positivity) (by norm_num) + have hαnonneg : 0 ≤ α := by dsimp [α]; positivity + have hα₂ : 2 ≤ α := by + have ha' : (4 : ℝ) ≤ a := by exact_mod_cast ha + nlinarith + have ht₁ : 1 ≤ t := by dsimp [t]; linarith + have htpos : 0 < t := lt_of_lt_of_le zero_lt_one ht₁ + have hα_eq : α = 2 * t := by dsimp [t]; ring + have ha_eq : (a : ℝ) = 4 * t ^ 2 := by rw [← hαpow, hα_eq]; ring + have hlog512 : Real.log 512 < (27 : ℝ) / 4 := by + calc + Real.log 512 = 9 * Real.log 2 := by + rw [show (512 : ℝ) = 2 ^ 9 by norm_num, Real.log_pow] + norm_num + _ < 9 * ((3 : ℝ) / 4) := + mul_lt_mul_of_pos_left log_two_lt_three_four (by norm_num) + _ = (27 : ℝ) / 4 := by norm_num + have hlog_eq : + Real.log (32 * (a : ℝ) ^ 2) = Real.log 512 + 4 * Real.log t := by + rw [ha_eq] + calc + Real.log (32 * (4 * t ^ 2) ^ 2) = Real.log (512 * t ^ 4) := by + congr 1 + ring + _ = Real.log 512 + Real.log (t ^ 4) := + Real.log_mul (by norm_num) (pow_ne_zero 4 htpos.ne') + _ = Real.log 512 + 4 * Real.log t := by rw [Real.log_pow]; norm_num + have hlogt : Real.log t ≤ t - 1 := Real.log_le_sub_one_of_pos htpos + have htarget : Real.log (32 * (a : ℝ) ^ 2) < (64 : ℝ) * t / 9 := by + rw [hlog_eq] + nlinarith + have hdenom : (1 + 2 * t) ^ 2 ≤ 9 * t ^ 2 := by + have hlin : 1 + 2 * t ≤ 3 * t := by linarith + exact pow_le_pow_left₀ (by positivity) hlin 2 |>.trans_eq (by ring) + have hlower : + (64 : ℝ) * t / 9 ≤ 8 * (a : ℝ) * α / (1 + α) ^ 2 := by + rw [ha_eq, hα_eq] + rw [div_le_div_iff₀ (by norm_num : (0 : ℝ) < 9) (sq_pos_of_pos (by linarith))] + nlinarith [mul_le_mul_of_nonneg_left hdenom (by positivity : (0 : ℝ) ≤ 64 * t / 9)] + exact htarget.trans_le hlower + +private lemma spectral_error_bound_n_two {a : ℕ} (ha : 4 ≤ a) : + let α : ℝ := (a : ℝ) ^ ((2 : ℝ)⁻¹) + let q : ℝ := + Real.sqrt (1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / 2)) / (1 + α) + q ^ (4 * a) < 1 / (32 * (a : ℝ) ^ 2) := by + let α : ℝ := (a : ℝ) ^ ((2 : ℝ)⁻¹) + let rad : ℝ := 1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / 2) + let q : ℝ := Real.sqrt rad / (1 + α) + let D : ℝ := (1 + α) ^ 2 + let u : ℝ := 4 * α / D + let P : ℝ := 8 * (a : ℝ) * α / D + have hαnonneg : 0 ≤ α := by dsimp [α]; positivity + have hrad : 0 ≤ rad := by + dsimp [rad] + rw [show (2 : ℝ) * Real.pi / 2 = Real.pi by ring, Real.cos_pi] + nlinarith [sq_nonneg (α - 1)] + have hq_sq : q ^ 2 = rad / D := by + dsimp [q, D] + rw [div_pow, Real.sq_sqrt hrad] + have hratio : rad / D = 1 - u := by + dsimp [rad, D, u] + rw [show (2 : ℝ) * Real.pi / 2 = Real.pi by ring, Real.cos_pi] + field_simp + ring + have hq_sq_exp : q ^ 2 ≤ Real.exp (-u) := by + rw [hq_sq, hratio] + exact Real.one_sub_le_exp_neg u + have hpowers : + (q ^ 2) ^ (2 * a) ≤ (Real.exp (-u)) ^ (2 * a) := + pow_le_pow_left₀ (sq_nonneg q) hq_sq_exp (2 * a) + have hpow_exp : q ^ (4 * a) ≤ Real.exp (-P) := by + calc + q ^ (4 * a) = (q ^ 2) ^ (2 * a) := by rw [show 4 * a = 2 * (2 * a) by ring, pow_mul] + _ ≤ (Real.exp (-u)) ^ (2 * a) := hpowers + _ = Real.exp ((2 * a : ℕ) * (-u)) := by rw [Real.exp_nat_mul] + _ = Real.exp (-P) := by + congr 1 + dsimp [u, P] + push_cast + field_simp + ring + have hexp : Real.exp (-P) < 1 / (32 * (a : ℝ) ^ 2) := by + apply exp_neg_lt_inv + · positivity + · simpa only [P, D, α] using exponent_two_gt_log ha + simpa only [q, rad, α] using hpow_exp.trans_lt hexp + +lemma spectral_error_bound {a n : ℕ} (ha : 4 ≤ a) (hn : 1 < n) + (ha₀ : 2 ^ (n - 1) ≤ a) : + let α : ℝ := (a : ℝ) ^ ((n : ℝ)⁻¹) + let q : ℝ := + Real.sqrt (1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / n)) / (1 + α) + (n - 1 : ℕ) * q ^ (2 * a * n) < + 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) := by + have hn2le : 2 ≤ n := by omega + rcases eq_or_lt_of_le hn2le with hn2 | hn3 + · subst n + have hexponent : (2 * a * 2 : ℕ) = 4 * a := by ring + rw [hexponent] + norm_num only [Nat.cast_ofNat, Nat.reduceSubDiff, one_mul] + simpa only [one_div] using spectral_error_bound_n_two ha + · exact spectral_error_bound_n_ge_three (by omega) ha₀ + +end ShuniaIntegerRoot From 773eee3ae30e2292829e384b74bbad93232a1a5e Mon Sep 17 00:00:00 2001 From: Ravi Bajaj Date: Fri, 24 Jul 2026 01:29:43 -0400 Subject: [PATCH 3/3] Optimize Shunia integer-root formalization Co-authored-by: Alexander Benjamin Worth Burns --- Mathlib/NumberTheory/ShuniaIntegerRoot.lean | 272 ++++++------------ .../ShuniaIntegerRoot/Estimates.lean | 152 ++++------ 2 files changed, 138 insertions(+), 286 deletions(-) diff --git a/Mathlib/NumberTheory/ShuniaIntegerRoot.lean b/Mathlib/NumberTheory/ShuniaIntegerRoot.lean index c2900f23e89b08..75bb2dcb4a3da4 100644 --- a/Mathlib/NumberTheory/ShuniaIntegerRoot.lean +++ b/Mathlib/NumberTheory/ShuniaIntegerRoot.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Ravi Bajaj and Ben Burns. All rights reserved. +Copyright (c) 2026 Ravi Bajaj and Alexander Benjamin Worth Burns. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Ravi Bajaj, Ben Burns +Authors: Ravi Bajaj, Alexander Benjamin Worth Burns -/ module @@ -11,7 +11,6 @@ import Mathlib.Algebra.BigOperators.ModEq import Mathlib.Algebra.Order.Floor.Semifield import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas -import Mathlib.Data.Nat.Choose.Sum /-! # Shunia's integer-root formula @@ -28,8 +27,6 @@ close to the positive real `n`-th root of `a`; evaluation at the large base `a ^ then recovers that ratio from the two modular residues. -/ -@[expose] public section - open scoped BigOperators namespace ShuniaIntegerRoot @@ -75,15 +72,12 @@ private lemma reducedEval_le_top_pow_mul_sum {a n k x : ℕ} (hn : 0 < n) (hx : ∑ i ∈ Finset.range n, coeff a n k i * x ^ (n - 1) := by apply Finset.sum_le_sum intro i hi - apply Nat.mul_le_mul_left - exact Nat.pow_le_pow_right hx (by - have := Finset.mem_range.mp hi - omega) + gcongr + have hi' := Finset.mem_range.mp hi + omega _ = x ^ (n - 1) * ∑ i ∈ Finset.range n, coeff a n k i := by rw [Finset.mul_sum] - apply Finset.sum_congr rfl - intro i hi - exact mul_comm _ _ + simp_rw [mul_comm] private def lowerEval (c : ℕ → ℕ) (n x : ℕ) : ℕ := ∑ i ∈ Finset.range (n - 1), c i * x ^ i @@ -141,7 +135,7 @@ private lemma lowerEval_error_le private lemma ratio_leading_error {U C Y L L' B Q : ℝ} (hU : 0 < U) (hC : 0 < C) (hY : 0 < Y) - (hL : 0 ≤ L) (hL' : 0 ≤ L') (hB : 0 ≤ B) + (hL : 0 ≤ L) (hL' : 0 ≤ L') (heD : L / (U * Y) ≤ B) (heN : L' / (C * Y) ≤ B) (hCU : C / U ≤ Q) : |(C * Y + L') / (U * Y + L) - C / U| ≤ Q * B := by @@ -149,8 +143,7 @@ private lemma ratio_leading_error let eN := L' / (C * Y) have heD0 : 0 ≤ eD := div_nonneg hL (mul_pos hU hY).le have heN0 : 0 ≤ eN := div_nonneg hL' (mul_pos hC hY).le - have heDB : eD ≤ B := heD - have heNB : eN ≤ B := heN + have hB : 0 ≤ B := heD0.trans heD have hden : 0 < 1 + eD := by linarith have hDY : U * Y + L = U * Y * (1 + eD) := by dsimp [eD] @@ -216,7 +209,7 @@ private lemma leading_recovery_of_decomposition (L := (lowerEval c n x : ℝ)) (L' := (lowerEval d n x : ℝ)) (B := 2 * n * a / x) (Q := 2 * a) (by exact_mod_cast hU) (by exact_mod_cast hC) (by positivity) - (by positivity) (by positivity) (by positivity) hec hed hCU.le + (by positivity) (by positivity) hec hed hCU.le push_cast at hratio ⊢ have hcoarse : (2 * (a : ℝ)) * (2 * n * a / x) < α / (4 * n * a ^ 2) := by have hxR : (0 : ℝ) < x := by positivity @@ -280,65 +273,38 @@ private lemma add_one_pow_mod_eq_reducedEval {a n k x : ℕ} (hn : 0 < n) (add_one_pow_modEq_reducedEval (k := k) hn (Nat.modEq_sub ha))).eq_of_lt_of_lt (Nat.mod_lt _ (Nat.zero_lt_of_lt hsmall)) hsmall -private def weight (a n i j : ℕ) : ℕ := - if j % n = i then a ^ (j / n) else 0 - -private lemma coeff_eq_sum_weight (a n k i : ℕ) : - coeff a n k i = - ∑ j ∈ Finset.range (k + 1), k.choose j * weight a n i j := by - simp only [coeff, weight] - rw [Finset.sum_filter] - apply Finset.sum_congr rfl - intro j hj - split_ifs <;> simp_all - -private lemma coeff_succ (a n k i : ℕ) : - coeff a n (k + 1) i = - coeff a n k i + - ∑ j ∈ Finset.range (k + 1), k.choose j * weight a n i (j + 1) := by - rw [coeff_eq_sum_weight, coeff_eq_sum_weight] - simpa using Finset.sum_choose_succ_mul (R := ℕ) (fun j _ ↦ weight a n i j) k - -private lemma weight_top_succ {a n j : ℕ} (hn : 1 < n) : - weight a n (n - 1) (j + 1) = weight a n (n - 2) j := by - unfold weight - have hn0 : 0 < n := by omega - have hmod : (j + 1) % n = n - 1 ↔ j % n = n - 2 := by - rw [Nat.add_mod] - rw [Nat.mod_eq_of_lt hn] - have hjmod : j % n < n := Nat.mod_lt _ hn0 - by_cases hlt : j % n + 1 < n - · rw [Nat.mod_eq_of_lt hlt] - omega - · have heq : j % n + 1 = n := by omega - rw [heq, Nat.mod_self] - omega - by_cases h : j % n = n - 2 - · rw [if_pos h, if_pos (hmod.mpr h)] - congr 1 - have hlt : j % n + 1 < n := by omega - have hdiv := Nat.add_div_eq_of_add_mod_lt - (a := j) (b := 1) (c := n) (by simpa [Nat.mod_eq_of_lt hn] using hlt) - simpa [Nat.div_eq_of_lt hn] using hdiv - · rw [if_neg h, if_neg (hmod.not.mpr h)] - private lemma coeff_succ_top {a n k : ℕ} (hn : 1 < n) : coeff a n (k + 1) (n - 1) = coeff a n k (n - 1) + coeff a n k (n - 2) := by - rw [coeff_succ, coeff_eq_sum_weight] - congr 1 - rw [coeff_eq_sum_weight] - apply Finset.sum_congr rfl - intro j hj - rw [weight_top_succ hn] + let w (i j : ℕ) := if j % n = i then a ^ (j / n) else 0 + have hcoeff (k i : ℕ) : + coeff a n k i = + ∑ j ∈ Finset.range (k + 1), k.choose j * w i j := by + simp [coeff, w, Finset.sum_filter] + have hshift (j : ℕ) : w (n - 1) (j + 1) = w (n - 2) j := by + dsimp [w] + have hmod : (j + 1) % n = n - 1 ↔ j % n = n - 2 := by + have hadd := Nat.add_mod_add_ite j 1 n + simp only [Nat.mod_eq_of_lt hn] at hadd + have hjmod := Nat.mod_lt j (by omega : 0 < n) + split at hadd <;> omega + by_cases h : j % n = n - 2 + · rw [if_pos h, if_pos (hmod.mpr h)] + congr 1 + have hlt : j % n + 1 < n := by omega + have hdiv := Nat.add_div_eq_of_add_mod_lt + (a := j) (b := 1) (c := n) (by simpa [Nat.mod_eq_of_lt hn] using hlt) + simpa [Nat.div_eq_of_lt hn] using hdiv + · rw [if_neg h, if_neg (hmod.not.mpr h)] + rw [hcoeff, hcoeff, hcoeff] + simpa [hshift] using + Finset.sum_choose_succ_mul (R := ℕ) (fun j _ ↦ w (n - 1) j) k private lemma four_mul_le_two_pow {a : ℕ} (ha : 4 ≤ a) : 4 * a ≤ 2 ^ a := by - obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le ha - induction d with - | zero => norm_num - | succ d ih => - rw [show 4 + (d + 1) = (4 + d) + 1 by omega, pow_succ] - have hpos : 1 ≤ 4 + d := by omega + induction a, ha using Nat.le_induction with + | base => norm_num + | succ a ha ih => + rw [pow_succ] omega /-- The positive real `n`-th root used in the spectral argument. -/ @@ -363,16 +329,14 @@ private lemma weighted_stdAddChar_sum {n i j : ℕ} [NeZero n] (hi : i < n) : rw [← AddChar.map_nsmul_eq_pow, ← AddChar.map_add_eq_mul] congr 1 ring - _ = if (j : ZMod n) - (i : ZMod n) = 0 then (n : ℂ) else 0 := by - simpa [mul_comm, ZMod.card] using - AddChar.sum_mulShift ((j : ZMod n) - (i : ZMod n)) - (ZMod.isPrimitive_stdAddChar n) - _ = if j % n = i then (n : ℂ) else 0 := by - split_ifs <;> - simp_all [sub_eq_zero, ZMod.natCast_eq_natCast_iff', Nat.mod_eq_of_lt hi] + _ = _ := by + simpa [mul_comm, ZMod.card, sub_eq_zero, ZMod.natCast_eq_natCast_iff', + Nat.mod_eq_of_lt hi] using + AddChar.sum_mulShift ((j : ZMod n) - (i : ZMod n)) + (ZMod.isPrimitive_stdAddChar n) private lemma spectral_sum_eq_filtered - (_a n k i : ℕ) (α : ℝ) [NeZero n] (hi : i < n) : + (n k i : ℕ) (α : ℝ) [NeZero n] (hi : i < n) : ∑ l : ZMod n, ZMod.stdAddChar (-((i : ZMod n) * l)) * (1 + (α : ℂ) * ZMod.stdAddChar l) ^ k = @@ -381,40 +345,29 @@ private lemma spectral_sum_eq_filtered (k.choose j : ℂ) * (α : ℂ) ^ j := by have hbin (z : ℂ) : (1 + z) ^ k = ∑ j ∈ Finset.range (k + 1), (k.choose j : ℂ) * z ^ j := by - rw [add_comm, add_pow] - apply Finset.sum_congr rfl - intro j hj - simp [mul_comm] + simpa [mul_comm, add_comm] using add_pow z 1 k calc _ = ∑ l : ZMod n, ZMod.stdAddChar (-((i : ZMod n) * l)) * ∑ j ∈ Finset.range (k + 1), (k.choose j : ℂ) * ((α : ℂ) * ZMod.stdAddChar l) ^ j := by - apply Finset.sum_congr rfl - intro l hl - rw [hbin] + simp_rw [hbin] _ = ∑ j ∈ Finset.range (k + 1), ((k.choose j : ℂ) * (α : ℂ) ^ j) * ∑ l : ZMod n, ZMod.stdAddChar (-((i : ZMod n) * l)) * ZMod.stdAddChar l ^ j := by - simp_rw [Finset.mul_sum] + simp_rw [Finset.mul_sum, mul_pow] rw [Finset.sum_comm] - apply Finset.sum_congr rfl - intro j hj - apply Finset.sum_congr rfl - intro l hl - rw [mul_pow] + congr 1 with j + congr 1 with l ring _ = ∑ j ∈ Finset.range (k + 1), ((k.choose j : ℂ) * (α : ℂ) ^ j) * (if j % n = i then (n : ℂ) else 0) := by - apply Finset.sum_congr rfl - intro j hj - rw [weighted_stdAddChar_sum hi] + simp_rw [weighted_stdAddChar_sum hi] _ = _ := by rw [Finset.sum_filter, Finset.mul_sum] - apply Finset.sum_congr rfl - intro j hj + congr 1 with j split_ifs <;> ring private lemma filtered_sum_eq_coeff_mul @@ -445,7 +398,7 @@ private lemma coeff_spectral_identity ∑ l : ZMod n, ZMod.stdAddChar (-((i : ZMod n) * l)) * (1 + (α : ℂ) * ZMod.stdAddChar l) ^ k := by - rw [spectral_sum_eq_filtered a n k i α hi, filtered_sum_eq_coeff_mul a n k i α hα] + rw [spectral_sum_eq_filtered n k i α hi, filtered_sum_eq_coeff_mul a n k i α hα] ring private lemma sin_pi_div_le_sin_mul {n r : ℕ} (hn : 0 < n) (hr : 0 < r) @@ -589,30 +542,17 @@ private lemma root_le_sqrt {a n : ℕ} (ha : 1 ≤ a) (hn : 2 ≤ n) : apply Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast ha) exact inv_anti₀ (by norm_num : (0 : ℝ) < 2) (by exact_mod_cast hn) -private lemma nthRoot_lt_root {a n : ℕ} (ha : 0 < a) (hn : n ≠ 0) +private lemma root_mem_Ioo_nthRoot_succ {a n : ℕ} (ha : 0 < a) (hn : n ≠ 0) (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) : - (n.nthRoot a : ℝ) < root a n := by - have hle : n.nthRoot a ^ n ≤ a := Nat.pow_nthRoot_le (.inl hn) - have hne : n.nthRoot a ^ n ≠ a := fun h ↦ hnotpow ⟨n.nthRoot a, h⟩ - have hlt : n.nthRoot a ^ n < a := lt_of_le_of_ne hle hne - have hlt' : (n.nthRoot a : ℝ) ^ n < (a : ℝ) := by exact_mod_cast hlt - rw [← root_pow ha hn] at hlt' - exact (pow_lt_pow_iff_left₀ (by positivity) (root_pos ha).le hn).mp hlt' - -private lemma root_lt_nthRoot_add_one {a n : ℕ} (ha : 0 < a) (hn : n ≠ 0) : - root a n < n.nthRoot a + 1 := by - have hlt := Nat.lt_pow_nthRoot_add_one hn a - have hlt' : (a : ℝ) < ((n.nthRoot a + 1 : ℕ) : ℝ) ^ n := by exact_mod_cast hlt - rw [← root_pow ha hn] at hlt' - push_cast at hlt' - exact (pow_lt_pow_iff_left₀ (root_pos ha).le (by positivity) hn).mp hlt' - -private lemma root_le_nat {a n : ℕ} (ha : 1 < a) (hn : 0 < n) : - root a n ≤ a := by - calc - root a n = root a n ^ 1 := by simp - _ ≤ root a n ^ n := pow_le_pow_right₀ (one_lt_root ha hn).le hn - _ = a := root_pow (by omega) hn.ne' + root a n ∈ Set.Ioo (n.nthRoot a : ℝ) (n.nthRoot a + 1) := by + constructor + · rw [root, Real.lt_rpow_inv_iff_of_pos (by positivity) (by positivity) + (by exact_mod_cast Nat.pos_of_ne_zero hn), Real.rpow_natCast] + exact_mod_cast lt_of_le_of_ne (Nat.pow_nthRoot_le (.inl hn)) + (fun h ↦ hnotpow ⟨n.nthRoot a, h⟩) + · rw [root, Real.rpow_inv_lt_iff_of_pos (by positivity) (by positivity) + (by exact_mod_cast Nat.pos_of_ne_zero hn), Real.rpow_natCast] + exact_mod_cast Nat.lt_pow_nthRoot_add_one hn a private lemma cast_sum_coeff_le {a n k : ℕ} (ha : 1 < a) (hn : 0 < n) : (∑ i ∈ Finset.range n, coeff a n k i : ℕ) ≤ (1 + root a n) ^ k := by @@ -758,9 +698,7 @@ private lemma coeff_ratio_close {a n k i j : ℕ} have hjk : j ≤ k := by calc j ≤ n := hj.le - _ = 1 * n := by simp - _ ≤ (2 * a) * n := Nat.mul_le_mul_right n (by omega) - _ = 2 * a * n := by ring + _ ≤ 2 * a * n := by nlinarith _ ≤ k := hk have hcj : 0 < coeff a n k j := coeff_pos_of_lt_of_le hj hjk have hε : 0 < ε := by dsimp [ε]; positivity @@ -780,9 +718,7 @@ private lemma coeff_ratio_close {a n k i j : ℕ} coeff_normalized_close ha hn hpow hj hk have hratio := normalized_ratio_close hε hεsmall hsi hsj have hpowSplit : α ^ j = α ^ i * α ^ (j - i) := by - rw [← pow_add] - congr 1 - omega + rw [← pow_add, Nat.add_sub_of_le hij] have hrelation : (coeff a n k i : ℝ) / coeff a n k j = α ^ (j - i) * (si / sj) := by @@ -853,7 +789,6 @@ private lemma reducedEval_lt_modulus {a n k : ℕ} (ha : 4 ≤ a) (hn : 1 < n) calc 4 * a ≤ (2 * n) * a := Nat.mul_le_mul_right a (by omega) _ = K := by simp [K]; ring - have hK2 : 2 ≤ K := le_trans (by omega : 2 ≤ 4 * a) hK4a have hx0 : 0 < x := by exact pow_pos ha0 _ have hbase0 : (0 : ℝ) ≤ 3 / 4 := by norm_num @@ -929,12 +864,10 @@ private lemma reducedEval_lt_modulus {a n k : ℕ} (ha : 4 ≤ a) (hn : 1 < n) rw [← pow_succ, Nat.sub_add_cancel hn0] have hdouble : 2 * reducedEval a n k x < x ^ n := by exact_mod_cast hdoubleReal - have ha2 : 2 * a < a ^ 2 := by nlinarith - have hax : a ^ 2 ≤ x := by - exact Nat.pow_le_pow_right ha0 hK2 - have hxn : x ≤ x ^ n := by - simpa using Nat.pow_le_pow_right hx0 (show 1 ≤ n by omega) - have haSmall : 2 * a < x ^ n := lt_of_lt_of_le ha2 (hax.trans hxn) + have haSmall : 2 * a < x ^ n := (show 2 * a < a ^ 2 by nlinarith).trans_le <| by + dsimp [x, K] + rw [← pow_mul] + exact Nat.pow_le_pow_right ha0 (by nlinarith) change reducedEval a n k x < x ^ n - a omega @@ -948,8 +881,7 @@ private lemma root_separation {a n : ℕ} (ha : 2 < a) (hn : 1 < n) have hn0 : n ≠ 0 := by omega have hα0 : 0 < α := root_pos ha0 have hα1 : 1 < α := one_lt_root (by omega) (by omega) - have hrα : (r : ℝ) < α := nthRoot_lt_root ha0 hn0 hnotpow - have hαr : α < (r : ℝ) + 1 := root_lt_nthRoot_add_one ha0 hn0 + have ⟨hrα, hαr⟩ := root_mem_Ioo_nthRoot_succ ha0 hn0 hnotpow have hr0 : (0 : ℝ) ≤ r := by positivity have hrootpow : α ^ n = (a : ℝ) := root_pow ha0 hn0 have hrootpowpred : α * α ^ (n - 1) = (a : ℝ) := by @@ -1034,9 +966,8 @@ private lemma div_sub_one_eq_nthRoot_of_approx {a n N D : ℕ} have hα0 : 0 < root a n := root_pos (by omega) have hhalf : root a n / (2 * n * a ^ 2) < root a n / (n * a ^ 2) := by - apply div_lt_div_of_pos_left hα0 - · positivity - · nlinarith [show (0 : ℝ) < n * a ^ 2 by positivity] + gcongr + nlinarith [show (0 : ℝ) < n by positivity] have habs := abs_lt.mp happrox have hlo : (n.nthRoot a : ℝ) < (N : ℝ) / (D : ℝ) - 1 := by have := hsep.1 @@ -1051,16 +982,6 @@ private lemma div_sub_one_eq_nthRoot_of_approx {a n N D : ℕ} rw [Nat.floor_div_eq_div] at hf omega -private lemma shunia_integer_root_three_two : - let k := 2 * 3 * 2 - let x := 3 ^ k - let m := x ^ 2 - 3 - Nat.nthRoot 2 3 = - ((x + 1) ^ (k + 1) % m) / ((x + 1) ^ k % m) - 1 := by - have hroot : Nat.nthRoot 2 3 = 1 := by decide - rw [hroot] - norm_num [Nat.pow_mod] - private lemma shunia_integer_root_of_four_le (a n : ℕ) (ha : 4 ≤ a) (hn : 1 < n) (hlog : n ≤ Nat.log2 a + 1) @@ -1087,22 +1008,14 @@ private lemma shunia_integer_root_of_four_le have hna : n ≤ a := by have := (n - 1).lt_two_pow_self omega - have hKtop : n - 1 ≤ K := by - calc - n - 1 ≤ n := Nat.sub_le n 1 - _ = 1 * n := by simp - _ ≤ (2 * a) * n := Nat.mul_le_mul_right n (by omega) - _ = K := by simp [K] - have hKpos : 1 ≤ K := by - dsimp [K] - nlinarith - have hX0 : 0 < X := by simp [X, ha0] - have haX : a ≤ X := by - dsimp [X] - simpa using Nat.pow_le_pow_right ha0 hKpos - have hXXn : X ≤ X ^ n := by - simpa using Nat.pow_le_pow_right hX0 (show 1 ≤ n by omega) - have haXn : a ≤ X ^ n := haX.trans hXXn + have hKtop : n - 1 ≤ K := + (Nat.sub_le n 1).trans <| by + dsimp [K] + nlinarith + have haXn : a ≤ X ^ n := by + simpa [X, K, ← pow_mul] using Nat.pow_le_pow_right ha0 + (Nat.one_le_iff_ne_zero.mpr (by positivity) : + 1 ≤ (2 * a * n) * n) have hsmallK : reducedEval a n K X < M := by simpa [K, X, M] using (reducedEval_lt_modulus (a := a) (n := n) (k := 2 * a * n) @@ -1135,34 +1048,25 @@ private lemma shunia_integer_root_of_four_le 2 * root a n ^ (n - 1 - i) := by intro i hi exact (coeff_ratio_close ha hn hpow (by omega) (by omega) (by simp [K])).2 + have hcoeffRatio := + coeff_ratio_close (a := a) (n := n) (k := K) (i := n - 2) (j := n - 1) + ha hn hpow (by omega) (by omega) (by simp [K]) have hcoeff : |(V : ℝ) / U - root a n| < root a n / (4 * n * a ^ 2) := by simpa [U, V, show n - 1 - (n - 2) = 1 by omega] using - (coeff_ratio_close (a := a) (n := n) (k := K) (i := n - 2) (j := n - 1) - ha hn hpow (by omega) (by omega) (by simp [K])).1 + hcoeffRatio.1 + have hVUtwo : (V : ℝ) / U < 2 * root a n := by + simpa [U, V, show n - 1 - (n - 2) = 1 by omega] using + hcoeffRatio.2 have hrec : C = U + V := by simpa [C, U, V] using coeff_succ_top (a := a) (n := n) (k := K) hn have hCUeq : (C : ℝ) / U = 1 + (V : ℝ) / U := by rw [hrec] push_cast field_simp [show (U : ℝ) ≠ 0 by exact_mod_cast hU.ne'] - have herrorOne : root a n / (4 * n * a ^ 2) < 1 := by - apply (div_lt_one (by positivity)).2 - have hrootA := root_le_nat (a := a) (n := n) (by omega) hn0 - have hlarge : (a : ℝ) < 4 * n * (a : ℝ) ^ 2 := by - have hfactor : (1 : ℝ) < 4 * n * a := by - have hn2 : (2 : ℝ) ≤ n := by exact_mod_cast (show 2 ≤ n by omega) - have ha4 : (4 : ℝ) ≤ a := by exact_mod_cast ha - nlinarith - nlinarith [mul_pos (show (0 : ℝ) < a by positivity) - (sub_pos.mpr hfactor)] - exact hrootA.trans_lt hlarge have hCU : (C : ℝ) / U < 2 * a := by - have hVU : (V : ℝ) / U < root a n + 1 := by - have := (abs_lt.mp hcoeff).2 - linarith rw [hCUeq] - have hrootA := root_le_nat (a := a) (n := n) (by omega) hn0 + have hrootBound := one_add_root_le_three_quarters ha (by omega : 2 ≤ n) have haR : (4 : ℝ) ≤ a := by exact_mod_cast ha nlinarith have heval : @@ -1196,7 +1100,7 @@ private lemma shunia_integer_root_of_four_le exact hrootResult.symm /-- Shunia's integer-root formula, formerly Conjecture 6.1. -/ -theorem shunia_integer_root +public theorem shunia_integer_root (a n : ℕ) (ha : 2 < a) (hn : 1 < n) (hlog : n ≤ Nat.log2 a + 1) (hnotpow : ¬ ∃ b : ℕ, b ^ n = a) : @@ -1214,6 +1118,8 @@ theorem shunia_integer_root rw [hlog3] at hlog omega subst n - exact shunia_integer_root_three_two + have hroot : Nat.nthRoot 2 3 = 1 := by decide + rw [hroot] + norm_num [Nat.pow_mod] end ShuniaIntegerRoot diff --git a/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean b/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean index f87a9d5c336764..50f55f1e3e13fe 100644 --- a/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean +++ b/Mathlib/NumberTheory/ShuniaIntegerRoot/Estimates.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Ravi Bajaj and Ben Burns. All rights reserved. +Copyright (c) 2026 Ravi Bajaj and Alexander Benjamin Worth Burns. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Ravi Bajaj, Ben Burns +Authors: Ravi Bajaj, Alexander Benjamin Worth Burns -/ module @@ -20,8 +20,6 @@ then, under the admissibility hypotheses, `(n - 1) * q ^ (2 * a * n)` is smaller `1 / (16 * n * a ^ 2)`. -/ -@[expose] public section - open Real namespace ShuniaIntegerRoot @@ -77,25 +75,19 @@ private lemma baseline_exponent_bound {n : ℕ} (hn : 3 ≤ n) : · norm_num only [Nat.cast_ofNat, Nat.cast_sub (by omega), Nat.cast_one, Nat.reduceSubDiff, Nat.reducePow, Nat.cast_pow] rw [Real.log_lt_iff_lt_exp (by norm_num)] - have he : (8 / 3 : ℝ) < Real.exp 1 := eight_thirds_lt_exp_one - have hp : (8 / 3 : ℝ) ^ 8 < (Real.exp 1) ^ 8 := by - exact pow_lt_pow_left₀ he (by positivity) (by norm_num) - have hp' : (8 / 3 : ℝ) ^ 8 < Real.exp 8 := by + have hp : (8 / 3 : ℝ) ^ 8 < Real.exp 8 := by calc - _ < (Real.exp 1) ^ 8 := hp + _ < (Real.exp 1) ^ 8 := + pow_lt_pow_left₀ eight_thirds_lt_exp_one (by positivity) (by norm_num) _ = Real.exp 8 := by rw [← Real.exp_nat_mul]; norm_num - exact (by norm_num : (1536 : ℝ) < (8 / 3) ^ 8).trans hp' - · have hn4' : 4 ≤ n := by omega - have htarget_nat := baseline_target_le_two_pow (show 1 ≤ n by omega) - have htarget : + exact (by norm_num : (1536 : ℝ) < (8 / 3) ^ 8).trans hp + · have htarget : (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) ≤ (2 : ℝ) ^ (4 * n) := by - exact_mod_cast htarget_nat + exact_mod_cast baseline_target_le_two_pow (show 1 ≤ n by omega) have hpos : 0 < 16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2 := by - have hnpos : (0 : ℝ) < n := by positivity - have hn1pos : (0 : ℝ) < (n - 1 : ℕ) := by - exact_mod_cast (show 0 < n - 1 by omega) + have hn1pos : 0 < n - 1 := by omega positivity have hlog : Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * ((2 : ℝ) ^ (n - 1)) ^ 2) ≤ @@ -113,21 +105,16 @@ private lemma baseline_exponent_bound {n : ℕ} (hn : 3 ≤ n) : _ < (4 * n : ℝ) * ((3 : ℝ) / 4) := mul_lt_mul_of_pos_left log_two_lt_three_four (by positivity) _ = 3 * n := by ring - have hsquare := nat_sq_le_two_pow hn4' - have hsquare' : (n : ℝ) ^ 2 ≤ (2 : ℝ) ^ n := by exact_mod_cast hsquare + have hsquare' : (n : ℝ) ^ 2 ≤ (2 : ℝ) ^ n := by + exact_mod_cast nat_sq_le_two_pow (show 4 ≤ n by omega) have hL : (3 : ℝ) * n ≤ 6 * (2 : ℝ) ^ (n - 1) / n := by rw [le_div_iff₀ (by positivity : (0 : ℝ) < n)] - have hp : (2 : ℝ) ^ n = 2 * (2 : ℝ) ^ (n - 1) := by - calc - (2 : ℝ) ^ n = 2 ^ ((n - 1) + 1) := by - congr 1 - omega - _ = 2 ^ (n - 1) * 2 := by rw [pow_succ] - _ = 2 * 2 ^ (n - 1) := by ring calc 3 * (n : ℝ) * n = 3 * (n : ℝ) ^ 2 := by ring _ ≤ 3 * (2 : ℝ) ^ n := by gcongr - _ = 6 * (2 : ℝ) ^ (n - 1) := by rw [hp]; ring + _ = 6 * (2 : ℝ) ^ (n - 1) := by + rw [← mul_pow_sub_one (n := n) (by omega) (2 : ℝ)] + ring exact hlog3.trans_le hL private lemma two_ninths_le_root_factor {x : ℝ} (hx₁ : 1 ≤ x) (hx₂ : x ≤ 2) : @@ -154,26 +141,20 @@ private lemma exponent_gt_log_of_pow {a n : ℕ} {α : ℝ} let L : ℝ := 6 * A / n let R : ℝ := Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * A ^ 2) have hApos : 0 < A := by dsimp [A]; positivity - have hnpos : (0 : ℝ) < n := by positivity - have hn1pos : (0 : ℝ) < (n - 1 : ℕ) := by - exact_mod_cast (show 0 < n - 1 by omega) + have hn1pos : 0 < n - 1 := by omega have haNat : 0 < a := lt_of_lt_of_le (by positivity : 0 < 2 ^ (n - 1)) ha₀ - have hapos : (0 : ℝ) < a := by exact_mod_cast haNat - have hαpos : 0 < α := lt_of_lt_of_le zero_lt_one hα₁ have hR_L : R < L := by simpa only [A, L, R] using baseline_exponent_bound hn - have hnA := nat_le_two_pow_pred (show 1 ≤ n by omega) have hnA' : (n : ℝ) ≤ A := by dsimp [A] - exact_mod_cast hnA + exact_mod_cast nat_le_two_pow_pred (show 1 ≤ n by omega) have hL6 : 6 ≤ L := by dsimp [L] - rw [le_div_iff₀ hnpos] + rw [le_div_iff₀ (by positivity : (0 : ℝ) < n)] nlinarith - have hLpos : 0 < L := lt_of_lt_of_le (by norm_num) hL6 rcases le_total α 2 with hα₂ | hα₂ · let s : ℝ := (a : ℝ) / A - have hspos : 0 < s := div_pos hapos hApos + have hspos : 0 < s := by dsimp [s]; positivity have hs₁ : 1 ≤ s := by dsimp [s] rw [le_div_iff₀ hApos] @@ -218,21 +199,13 @@ private lemma exponent_gt_log_of_pow {a n : ℕ} {α : ℝ} L * s = 6 * (a : ℝ) / n := by rw [ha_eq]; simp [L]; ring _ ≤ _ := hP · let t : ℝ := α / 2 - have htpos : 0 < t := div_pos hαpos (by norm_num) + have htpos : 0 < t := div_pos (zero_lt_one.trans_le hα₁) (by norm_num) have ht₁ : 1 ≤ t := by dsimp [t]; linarith have hα_eq : α = 2 * t := by dsimp [t]; ring have ha_eq : (a : ℝ) = A * (2 * t ^ n) := by rw [← hαpow, hα_eq] dsimp [A] - rw [mul_pow] - have htwo : (2 : ℝ) ^ n = 2 * 2 ^ (n - 1) := by - calc - (2 : ℝ) ^ n = 2 ^ ((n - 1) + 1) := by - congr 1 - omega - _ = 2 ^ (n - 1) * 2 := by rw [pow_succ] - _ = 2 * 2 ^ (n - 1) := by ring - rw [htwo] + rw [mul_pow, ← mul_pow_sub_one (n := n) (by omega) (2 : ℝ)] ring have hlog_eq : Real.log (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) = @@ -275,12 +248,12 @@ private lemma exponent_gt_log_of_pow {a n : ℕ} {α : ℝ} _ ≤ 6 * (1 + (n - 1 : ℕ) * (t - 1)) := hlinear _ ≤ 6 * t ^ (n - 1) := by gcongr _ ≤ L * t ^ (n - 1) := by gcongr - have ht_pow_one : 1 ≤ t ^ (n - 1) := one_le_pow₀ ht₁ have htotal : R + 2 * Real.log 2 + 2 * n * Real.log t < 2 * L * t ^ (n - 1) := by have hfirst : R < L * t ^ (n - 1) := - hR_L.trans_le (by simpa using mul_le_mul_of_nonneg_left ht_pow_one hLpos.le) + hR_L.trans_le (by simpa using + mul_le_mul_of_nonneg_left (one_le_pow₀ ht₁) (by linarith [hL6])) nlinarith have hfac := four_ninths_div_le_root_factor hα₂ have hP : @@ -296,8 +269,7 @@ private lemma exponent_gt_log_of_pow {a n : ℕ} {α : ℝ} 2 * L * t ^ (n - 1) = 12 * (a : ℝ) / ((n : ℝ) * α) := by rw [ha_eq, hα_eq] dsimp [L] - rw [show t ^ n = t ^ (n - 1) * t by - conv_lhs => rw [show n = (n - 1) + 1 by omega, pow_succ]] + rw [← pow_sub_one_mul (n := n) (by omega) t] field_simp ring rw [hlog_eq] @@ -305,17 +277,14 @@ private lemma exponent_gt_log_of_pow {a n : ℕ} {α : ℝ} private lemma sin_pi_div_lower {n : ℕ} (hn : 3 ≤ n) : (3 * Real.sqrt 3) / (2 * n) ≤ Real.sin (Real.pi / n) := by - have hlam0 : (0 : ℝ) ≤ 3 / n := by positivity have hlam1 : (3 : ℝ) / n ≤ 1 := by rw [div_le_one (by positivity : (0 : ℝ) < n)] exact_mod_cast hn - have hpi3 : Real.pi / 3 ∈ Set.Icc (0 : ℝ) Real.pi := by - constructor - · positivity - · nlinarith [Real.pi_pos] + have hpi3 : Real.pi / 3 ∈ Set.Icc (0 : ℝ) Real.pi := + ⟨by positivity, by nlinarith [Real.pi_pos]⟩ have hc := strictConcaveOn_sin_Icc.concaveOn.2 (show (0 : ℝ) ∈ Set.Icc (0 : ℝ) Real.pi by simp [Real.pi_pos.le]) - hpi3 (sub_nonneg.mpr hlam1) hlam0 + hpi3 (sub_nonneg.mpr hlam1) (show (0 : ℝ) ≤ 3 / n by positivity) calc (3 * Real.sqrt 3) / (2 * n) = (3 / n) * (Real.sqrt 3 / 2) := by ring _ ≤ Real.sin (Real.pi / n) := by @@ -323,22 +292,15 @@ private lemma sin_pi_div_lower {n : ℕ} (hn : 3 ≤ n) : private lemma one_sub_cos_two_pi_div_lower {n : ℕ} (hn : 3 ≤ n) : (27 : ℝ) / (2 * n ^ 2) ≤ 1 - Real.cos (2 * Real.pi / n) := by - have hsin := sin_pi_div_lower hn - have hlower_nonneg : (0 : ℝ) ≤ (3 * Real.sqrt 3) / (2 * n) := by positivity have hsin_sq : ((3 * Real.sqrt 3) / (2 * n)) ^ 2 ≤ (Real.sin (Real.pi / n)) ^ 2 := - pow_le_pow_left₀ hlower_nonneg hsin 2 - have hsqrt : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num) - have htrig : - 1 - Real.cos (2 * Real.pi / n) = 2 * (Real.sin (Real.pi / n)) ^ 2 := by - rw [show 2 * Real.pi / (n : ℝ) = 2 * (Real.pi / n) by ring, - Real.sin_sq_eq_half_sub] - ring - rw [htrig] + pow_le_pow_left₀ (by positivity) (sin_pi_div_lower hn) 2 + rw [show 2 * Real.pi / (n : ℝ) = 2 * (Real.pi / n) by ring, + Real.cos_two_mul_eq_one_sub] rw [div_pow] at hsin_sq have hn0 : (n : ℝ) ≠ 0 := by positivity field_simp [hn0] at hsin_sq ⊢ - nlinarith [hsqrt] + nlinarith [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)] private lemma spectral_error_bound_n_ge_three {a n : ℕ} (hn : 3 ≤ n) (ha₀ : 2 ^ (n - 1) ≤ a) : @@ -355,17 +317,12 @@ private lemma spectral_error_bound_n_ge_three {a n : ℕ} (hn : 3 ≤ n) let u : ℝ := 2 * α * (1 - c) / D let v : ℝ := 27 * α / ((n : ℝ) ^ 2 * D) let P : ℝ := 27 * (a : ℝ) * α / ((n : ℝ) * D) - have hapos : (0 : ℝ) < a := by - exact_mod_cast lt_of_lt_of_le (by positivity : 0 < 2 ^ (n - 1)) ha₀ + have ha₁ : 1 ≤ a := (show 1 ≤ n by omega).trans + ((nat_le_two_pow_pred (show 1 ≤ n by omega)).trans ha₀) + have hapos : 0 < a := by omega have hα₁ : 1 ≤ α := by dsimp [α] - apply Real.one_le_rpow - · exact_mod_cast (show 1 ≤ n by omega).trans - ((nat_le_two_pow_pred (show 1 ≤ n by omega)).trans ha₀) - · positivity - have hαpos : 0 < α := lt_of_lt_of_le zero_lt_one hα₁ - have hnpos : (0 : ℝ) < n := by positivity - have hDpos : 0 < D := by dsimp [D]; positivity + exact Real.one_le_rpow (by exact_mod_cast ha₁) (by positivity) have hrad : 0 ≤ rad := by have hc := Real.neg_one_le_cos (2 * Real.pi / (n : ℝ)) dsimp [rad, c] @@ -392,14 +349,11 @@ private lemma spectral_error_bound_n_ge_three {a n : ℕ} (hn : 3 ≤ n) rw [hq_sq, hratio] exact (Real.one_sub_le_exp_neg u).trans (Real.exp_le_exp.mpr (neg_le_neg huv)) have hpow_exp : q ^ (2 * a * n) ≤ Real.exp (-P) := by - have hpowers : - (q ^ 2) ^ (a * n) ≤ (Real.exp (-v)) ^ (a * n) := - pow_le_pow_left₀ (sq_nonneg q) hq_sq_exp (a * n) - have hexponent : (2 * a * n : ℕ) = 2 * (a * n) := by simp [mul_assoc] calc q ^ (2 * a * n) = (q ^ 2) ^ (a * n) := by - rw [hexponent, pow_mul] - _ ≤ (Real.exp (-v)) ^ (a * n) := hpowers + simpa [mul_assoc] using pow_mul q 2 (a * n) + _ ≤ (Real.exp (-v)) ^ (a * n) := + pow_le_pow_left₀ (sq_nonneg q) hq_sq_exp (a * n) _ = Real.exp ((a * n : ℕ) * (-v)) := by rw [Real.exp_nat_mul] _ = Real.exp (-P) := by @@ -407,27 +361,23 @@ private lemma spectral_error_bound_n_ge_three {a n : ℕ} (hn : 3 ≤ n) dsimp [v, P] push_cast field_simp + have hn1 : n - 1 ≠ 0 := by omega have hexp : Real.exp (-P) < 1 / (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) := by apply exp_neg_lt_inv - · have : 0 < n - 1 := by omega - positivity + · positivity · simpa only [P, D, α] using exponent_gt_log_of_pow hn ha₀ hα₁ (Real.rpow_inv_natCast_pow (by positivity) (by omega)) - have hq : q ^ (2 * a * n) < - 1 / (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2) := by - exact hpow_exp.trans_lt hexp - have hn1pos : (0 : ℝ) < (n - 1 : ℕ) := by - exact_mod_cast (show 0 < n - 1 by omega) - have hmul := mul_lt_mul_of_pos_left hq hn1pos + have hmul := mul_lt_mul_of_pos_left (hpow_exp.trans_lt hexp) + (show (0 : ℝ) < (n - 1 : ℕ) by positivity) change (↑(n - 1) : ℝ) * q ^ (2 * a * n) < 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) calc (↑(n - 1) : ℝ) * q ^ (2 * a * n) < (↑(n - 1) : ℝ) * (1 / (16 * (n : ℝ) * (↑(n - 1) : ℝ) * (a : ℝ) ^ 2)) := hmul _ = 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) := by - field_simp + field_simp [hn1] private lemma exponent_two_gt_log {a : ℕ} (ha : 4 ≤ a) : let α : ℝ := (a : ℝ) ^ ((2 : ℝ)⁻¹) @@ -504,13 +454,12 @@ private lemma spectral_error_bound_n_two {a : ℕ} (ha : 4 ≤ a) : have hq_sq_exp : q ^ 2 ≤ Real.exp (-u) := by rw [hq_sq, hratio] exact Real.one_sub_le_exp_neg u - have hpowers : - (q ^ 2) ^ (2 * a) ≤ (Real.exp (-u)) ^ (2 * a) := - pow_le_pow_left₀ (sq_nonneg q) hq_sq_exp (2 * a) have hpow_exp : q ^ (4 * a) ≤ Real.exp (-P) := by calc - q ^ (4 * a) = (q ^ 2) ^ (2 * a) := by rw [show 4 * a = 2 * (2 * a) by ring, pow_mul] - _ ≤ (Real.exp (-u)) ^ (2 * a) := hpowers + q ^ (4 * a) = (q ^ 2) ^ (2 * a) := by + simpa [← mul_assoc] using pow_mul q 2 (2 * a) + _ ≤ (Real.exp (-u)) ^ (2 * a) := + pow_le_pow_left₀ (sq_nonneg q) hq_sq_exp (2 * a) _ = Real.exp ((2 * a : ℕ) * (-u)) := by rw [Real.exp_nat_mul] _ = Real.exp (-P) := by congr 1 @@ -524,18 +473,15 @@ private lemma spectral_error_bound_n_two {a : ℕ} (ha : 4 ≤ a) : · simpa only [P, D, α] using exponent_two_gt_log ha simpa only [q, rad, α] using hpow_exp.trans_lt hexp -lemma spectral_error_bound {a n : ℕ} (ha : 4 ≤ a) (hn : 1 < n) +public lemma spectral_error_bound {a n : ℕ} (ha : 4 ≤ a) (hn : 1 < n) (ha₀ : 2 ^ (n - 1) ≤ a) : let α : ℝ := (a : ℝ) ^ ((n : ℝ)⁻¹) let q : ℝ := Real.sqrt (1 + α ^ 2 + 2 * α * Real.cos (2 * Real.pi / n)) / (1 + α) (n - 1 : ℕ) * q ^ (2 * a * n) < 1 / (16 * (n : ℝ) * (a : ℝ) ^ 2) := by - have hn2le : 2 ≤ n := by omega - rcases eq_or_lt_of_le hn2le with hn2 | hn3 - · subst n - have hexponent : (2 * a * 2 : ℕ) = 4 * a := by ring - rw [hexponent] + rcases eq_or_lt_of_le (show 2 ≤ n by omega) with rfl | hn3 + · rw [show (2 * a * 2 : ℕ) = 4 * a by ring] norm_num only [Nat.cast_ofNat, Nat.reduceSubDiff, one_mul] simpa only [one_div] using spectral_error_bound_n_two ha · exact spectral_error_bound_n_ge_three (by omega) ha₀