2607.19283v1 / ENOTV/Bulk.lean
all files
import ENOTV.Estimates
import Mathlib.Topology.Algebra.Polynomial
/-!
# A uniform bulk region in an Euler block
For each fixed degree we select a rational point strictly inside `(0,1)`
where the Euler polynomial is nonzero, then use continuity to obtain a
degree-dependent interval on which it is bounded away from zero.
-/
noncomputable section
open Polynomial
namespace ENOTV
theorem eulerPoly_ne_zero (d : ℕ) : eulerPoly d ≠ 0 := by
intro h
have hid := eulerPoly_add_one d 1
simp [h] at hid
theorem exists_euler_nonzero_reciprocal (d : ℕ) :
∃ q : ℕ, 2 ≤ q ∧ q ≤ d + 2 ∧
(eulerPoly d).eval (1 / (q : ℚ)) ≠ 0 := by
let f : Fin (d + 1) → ℚ := fun i => 1 / (i.val + 2 : ℚ)
have hf : Function.Injective f := by
intro i j hij
apply Fin.ext
have hi : (i.val + 2 : ℚ) ≠ 0 := by positivity
have hj : (j.val + 2 : ℚ) ≠ 0 := by positivity
dsimp [f] at hij
field_simp [hi, hj] at hij
have hv : (i.val : ℚ) = (j.val : ℚ) := by linarith
exact_mod_cast hv
by_contra h
push Not at h
have hall : ∀ i : Fin (d + 1), (eulerPoly d).eval (f i) = 0 := by
intro i
simpa [f] using h (i.val + 2) (by omega) (by omega)
have hz : eulerPoly d = 0 := by
apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero
(eulerPoly d) hf hall
simpa using (eulerPoly_natDegree_le d).trans_lt (Nat.lt_succ_self d)
exact eulerPoly_ne_zero d hz
/-- A rational point and radius on which `|E_d|` is bounded from below by
half its value at the point. -/
theorem exists_euler_bulk_window (d : ℕ) :
∃ q : ℕ, ∃ δ : ℝ,
2 ≤ q ∧ 0 < δ ∧ 0 < |(eulerPoly d).eval (1 / (q : ℚ))| ∧
∀ x : ℚ, ((|x - 1 / (q : ℚ)| : ℚ) : ℝ) < δ →
|(eulerPoly d).eval (1 / (q : ℚ))| / 2 ≤
|(eulerPoly d).eval x| := by
obtain ⟨q, hq2, hqd, hne⟩ := exists_euler_nonzero_reciprocal d
let α : ℚ := 1 / q
let y : ℚ := |(eulerPoly d).eval α|
have hy : 0 < y := abs_pos.mpr hne
have hc : ContinuousAt (fun x : ℚ => (eulerPoly d).eval x) α :=
(eulerPoly d).continuousAt
obtain ⟨δ, hδ, hcont⟩ :=
Metric.continuousAt_iff.mp hc (y / 2) (by positivity)
refine ⟨q, δ, hq2, hδ, hy, ?_⟩
intro x hx
have hd : dist x α < δ := by
rw [Rat.dist_eq]
simpa [α, Rat.cast_abs] using hx
have hv := hcont hd
rw [Rat.dist_eq] at hv
have habs :
(|(eulerPoly d).eval α| : ℚ) - |(eulerPoly d).eval x| ≤
|(eulerPoly d).eval α - (eulerPoly d).eval x| :=
abs_sub_abs_le_abs_sub _ _
have habsR :
((|(eulerPoly d).eval α| : ℚ) : ℝ) -
((|(eulerPoly d).eval x| : ℚ) : ℝ) ≤
|(((eulerPoly d).eval α : ℚ) : ℝ) -
(((eulerPoly d).eval x : ℚ) : ℝ)| := by
exact_mod_cast habs
have hv' :
|(((eulerPoly d).eval α : ℚ) : ℝ) -
(((eulerPoly d).eval x : ℚ) : ℝ)| <
((|(eulerPoly d).eval α| : ℚ) : ℝ) / 2 := by
simpa [abs_sub_comm, y] using hv
simp only [Rat.cast_abs] at habsR hv'
have hreal :
(((|(eulerPoly d).eval α| / 2 : ℚ) : ℝ)) ≤
((|(eulerPoly d).eval x| : ℚ) : ℝ) := by
push_cast
nlinarith [habsR, hv']
dsimp [α] at hreal
exact_mod_cast hreal
/-- Along a fixed arithmetic subsequence of block lengths, each block has
linearly many samples of full `L^d` size. -/
theorem exists_bulk_samples (d : ℕ) :
∃ b a : ℕ, ∃ c : ℚ, 0 < b ∧ a < 2 * b ∧ 0 < c ∧
∀ M r : ℕ, 0 < M → r < M →
let L := b * M
let t := a * M + r
t < 2 * L ∧ c * (L : ℚ) ^ d ≤ |blockPoly d L t| := by
obtain ⟨q, δ, hq2, hδ, hy, hwin⟩ := exists_euler_bulk_window d
obtain ⟨n, hnδ⟩ := exists_nat_one_div_lt hδ
let s := n + 1
let b := q * s
let a := 2 * s
let y : ℚ := |(eulerPoly d).eval (1 / (q : ℚ))|
let c : ℚ := 2 ^ d * (y / 2)
have hy' : 0 < y := by simpa [y] using hy
refine ⟨b, a, c, ?_, ?_, by positivity, ?_⟩
· dsimp [b, s]
positivity
· dsimp [a, b]
have hs : 0 < s := by simp [s]
calc
2 * s < (2 * q) * s := Nat.mul_lt_mul_of_pos_right (by omega) hs
_ = 2 * (q * s) := by ring
intro M r hM hr
dsimp only
let L := b * M
let t := a * M + r
change t < 2 * L ∧ c * (L : ℚ) ^ d ≤ |blockPoly d L t|
have hL : 0 < L := by positivity
have ht : t < 2 * L := by
dsimp [t, L, b, a, s]
have hs0 : 0 < 2 * (n + 1) := by positivity
have hr2 : r < 2 * (n + 1) * M :=
hr.trans_le (Nat.le_mul_of_pos_left M hs0)
have hsum :
2 * (n + 1) * M + r <
2 * (n + 1) * M + 2 * (n + 1) * M :=
Nat.add_lt_add_left hr2 _
have hscale :
2 * (n + 1) * M + 2 * (n + 1) * M ≤
2 * (q * (n + 1) * M) := by
have hcoef : 4 ≤ 2 * q := by omega
have := Nat.mul_le_mul_right ((n + 1) * M) hcoef
nlinarith
exact hsum.trans_le hscale
refine ⟨ht, ?_⟩
have harg :
((|((t : ℚ) / (2 * L)) - 1 / (q : ℚ)| : ℚ) : ℝ) < δ := by
have hqpos : (0 : ℚ) < q := by positivity
have hspos : (0 : ℚ) < s := by positivity
have hMpos : (0 : ℚ) < M := by positivity
have hform :
(t : ℚ) / (2 * L) - 1 / (q : ℚ) =
(r : ℚ) / (2 * q * s * M) := by
dsimp [t, L, b, a]
field_simp
push_cast
ring
rw [hform, abs_of_nonneg (by positivity)]
have hrR : (r : ℝ) < M := by exact_mod_cast hr
have hdenR : (0 : ℝ) < 2 * q * s * M := by positivity
have hsmall :
(r : ℝ) / (2 * q * s * M) < 1 / (s : ℝ) := by
calc
(r : ℝ) / (2 * q * s * M) <
(M : ℝ) / (2 * q * s * M) := by
exact (div_lt_div_iff_of_pos_right hdenR).2 hrR
_ ≤ 1 / (s : ℝ) := by
have hsR : (0 : ℝ) < s := by positivity
apply (div_le_iff₀ hdenR).2
field_simp
have hqR : (2 : ℝ) ≤ q := by exact_mod_cast hq2
have hM0 : (0 : ℝ) < M := by exact_mod_cast hM
nlinarith
have hsδ : 1 / (s : ℝ) < δ := by simpa [s] using hnδ
have hcast :
((((r : ℚ) / (2 * q * s * M) : ℚ)) : ℝ) =
(r : ℝ) / (2 * q * s * M) := by
rw [Rat.cast_div (α := ℝ)]
push_cast
rfl
rw [hcast]
exact hsmall.trans hsδ
have hlower := hwin ((t : ℚ) / (2 * L)) harg
rw [blockPoly, abs_mul, abs_pow,
abs_of_nonneg (show (0 : ℚ) ≤ 2 * L by positivity)]
dsimp [c, y]
calc
2 ^ d * (|(eulerPoly d).eval (1 / (q : ℚ))| / 2) * (L : ℚ) ^ d =
(2 * (L : ℚ)) ^ d *
(|(eulerPoly d).eval (1 / (q : ℚ))| / 2) := by ring
_ ≤ (2 * (L : ℚ)) ^ d *
|(eulerPoly d).eval ((t : ℚ) / (2 * L))| := by gcongr
theorem cJumpMoment_eq_powerSum (k : ℕ) (u : CSeq) :
cJumpMoment k u = powerSum k (cdiff u) := rfl
/-- Quantitative bulk lower bound for one positive/negative pair. -/
theorem exists_pair_moment_lower (d k : ℕ) :
∃ b a : ℕ, ∃ c : ℚ, 0 < b ∧ a < 2 * b ∧ 0 < c ∧
∀ M : ℕ, 0 < M →
let L := b * M
(M : ℝ) * ((c : ℝ) * (L : ℝ) ^ d) ^ (k + 1) ≤
powerSum k (pairJumps d L) := by
obtain ⟨b, a, c, hb, hab, hc, hsamples⟩ := exists_bulk_samples d
refine ⟨b, a, c, hb, hab, hc, ?_⟩
intro M hM
dsimp only
let L := b * M
let emb : ℕ ↪ ℤ :=
⟨fun r => (a * M + r : ℕ), by
intro r s hrs
apply Nat.add_left_cancel
exact Int.ofNat_injective hrs⟩
let S : Finset ℤ := (Finset.range M).map emb
have hsample (r : ℕ) (hr : r < M) :
(c : ℝ) * (L : ℝ) ^ d ≤ |pairJumps d L (emb r)| := by
have hs := hsamples M r hM hr
dsimp only at hs
rcases hs with ⟨ht, hlow⟩
have hreal :
(c : ℝ) * (L : ℝ) ^ d ≤ |realBlock d L (a * M + r)| := by
unfold realBlock
exact_mod_cast hlow
change (c : ℝ) * (L : ℝ) ^ d ≤
|pairJumps d L ((a * M + r : ℕ) : ℤ)|
simp only [pairJumps, liftNat_apply_nat, pairJumpNat_apply]
rw [if_pos ht]
exact hreal
have hSsub : S ⊆ (pairJumps d L).support := by
intro i hi
rw [Finset.mem_map] at hi
obtain ⟨r, hr, rfl⟩ := hi
apply Finsupp.mem_support_iff.mpr
have hlower := hsample r (Finset.mem_range.mp hr)
have hcR : 0 < (c : ℝ) := by exact_mod_cast hc
have hLR : 0 < (L : ℝ) := by
dsimp [L]
positivity
have hpos : 0 < (c : ℝ) * (L : ℝ) ^ d := by positivity
intro hz
simp [hz] at hlower
linarith
rw [powerSum, Finsupp.sum]
calc
(M : ℝ) * ((c : ℝ) * (L : ℝ) ^ d) ^ (k + 1) =
∑ i ∈ S, ((c : ℝ) * (L : ℝ) ^ d) ^ (k + 1) := by
simp [S]
_ ≤ ∑ i ∈ S, |pairJumps d L i| ^ (k + 1) := by
apply Finset.sum_le_sum
intro i hi
rw [Finset.mem_map] at hi
obtain ⟨r, hr, rfl⟩ := hi
exact pow_le_pow_left₀ (by positivity)
(hsample r (Finset.mem_range.mp hr)) _
_ ≤ ∑ i ∈ (pairJumps d L).support,
|pairJumps d L i| ^ (k + 1) := by
apply Finset.sum_le_sum_of_subset_of_nonneg hSsub
intro i hiS hi
positivity
theorem exists_multi_moment_lower (d k : ℕ) :
∃ b : ℕ, ∃ c : ℚ, 0 < b ∧ 0 < c ∧
∀ M P : ℕ, 0 < M →
let L := b * M
(P : ℝ) * (M : ℝ) *
((c : ℝ) * (L : ℝ) ^ d) ^ (k + 1) ≤
cJumpMoment k (multiDatum d L P) := by
obtain ⟨b, a, c, hb, hab, hc, hlower⟩ :=
exists_pair_moment_lower d k
refine ⟨b, c, hb, hc, ?_⟩
intro M P hM
dsimp only
rw [cJumpMoment_eq_powerSum, cdiff_multiDatum,
powerSum_multiJumps]
have hp := hlower M hM
dsimp only at hp
have hP : 0 ≤ (P : ℝ) := by positivity
calc
(P : ℝ) * (M : ℝ) *
((c : ℝ) * ((b * M : ℕ) : ℝ) ^ d) ^ (k + 1) =
(P : ℝ) * ((M : ℝ) *
((c : ℝ) * ((b * M : ℕ) : ℝ) ^ d) ^ (k + 1)) := by ring
_ ≤ (P : ℝ) * powerSum k (pairJumps d (b * M)) := by gcongr
end ENOTV