NewtonDominance.lean

1 module
2 
3 public import GlobalEulerBoundary
4 public import Mathlib.NumberTheory.Padics.PadicVal.Basic
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace KomorebiPaperIX.NewtonDominance
11 
12 open Mahler GlobalEulerBoundary
13 
14 lemma precision_mono {L M : ℤ} {x : ℚ} (h : L ≤ M)
15     (hx : precision 2 M x) : precision 2 L x := by
16   rcases hx with hx | hx
17   · exact Or.inl hx
18   · exact Or.inr (h.trans hx)
19 
20 lemma precision_add {L : ℤ} {x y : ℚ}
21     (hx : precision 2 L x) (hy : precision 2 L y) : precision 2 L (x + y) := by
22   rcases hx with rfl | hx
23   · simpa using hy
24   rcases hy with rfl | hy
25   · rw [add_zero]
26     exact Or.inr hx
27   by_cases h : x + y = 0
28   · exact Or.inl h
29   · exact Or.inr ((le_min hx hy).trans (padicValRat.min_le_padicValRat_add h))
30 
31 lemma precision_sum {ι : Type*} (S : Finset ι) (g : ι → ℚ) (L : ℤ)
32     (H : ∀ i ∈ S, precision 2 L (g i)) : precision 2 L (∑ i ∈ S, g i) := by
33   classical
34   induction S using Finset.induction_on with
35   | empty => simp
36   | @insert i S hi ih =>
37     rw [Finset.sum_insert hi]
38     exact precision_add (H i (Finset.mem_insert_self _ _))
39       (ih (by intro j hj; exact H j (Finset.mem_insert_of_mem hj)))
40 
41 lemma precision_mul {L M : ℤ} {x y : ℚ}
42     (hx : precision 2 L x) (hy : precision 2 M y) : precision 2 (L + M) (x * y) := by
43   by_cases hxn : x = 0
44   · simp [hxn]
45   by_cases hyn : y = 0
46   · simp [hyn]
47   have hxv := hx.resolve_left hxn
48   have hyv := hy.resolve_left hyn
49   exact Or.inr (by rw [padicValRat.mul hxn hyn]; omega)
50 
51 lemma precision_mul_nat {L : ℤ} {x : ℚ} (hx : precision 2 L x) (b : ℕ) :
52     precision 2 L (x * (b : ℚ)) := by
53   simpa using precision_mul hx (Or.inr (zero_le_padicValRat_of_nat b) : precision 2 0 (b : ℚ))
54 
55 /-- A strictly higher precision perturbation cannot cancel the leading term. -/
56 lemma strict_dominance (x y : ℚ) (c : ℤ) (hx : x ≠ 0)
57     (hv : padicValRat 2 x = c) (hy : precision 2 (c + 1) y) :
58     x + y ≠ 0 ∧ padicValRat 2 (x + y) = c := by
59   rcases hy with rfl | hy
60   · simpa using And.intro hx hv
61   have hsum : x + y ≠ 0 := by
62     intro h
63     have heq : y = -x := by linarith
64     rw [heq, padicValRat.neg, hv] at hy
65     omega
66   by_cases hyn : y = 0
67   · simp [hyn, hx, hv]
68   exact ⟨hsum, (padicValRat.add_eq_of_lt hsum hx hyn (by omega)).trans hv⟩
69 
70 /-- Translation preserves a monotone lower envelope on the Newton coefficients. -/
71 lemma translated_tail (f : ℕ → ℚ) (c k n : ℕ) (hk : 2 ≤ k)
72     (H : ∀ i, 2 ≤ i → precision 2 ((c + 1 + Nat.log 2 i : ℕ) : ℤ) (coefficient f i)) :
73     precision 2 ((c + 1 + Nat.log 2 k : ℕ) : ℤ) (difference 1 k f n) := by
74   rw [difference_from_coefficients]
75   apply precision_sum
76   intro j _
77   apply precision_mul_nat
78   apply precision_mono _ (H (k + j) (by omega))
79   exact_mod_cast Nat.add_le_add_left (Nat.log_monotone (show k ≤ k + j by omega)) (c + 1)
80 
81 lemma first_difference_tail (f : ℕ → ℚ) (c n : ℕ)
82     (H : ∀ i, 2 ≤ i → precision 2 ((c + 1 + Nat.log 2 i : ℕ) : ℤ) (coefficient f i)) :
83     precision 2 ((c : ℤ) + 1) (difference 1 1 f n - coefficient f 1) := by
84   rw [difference_from_coefficients, Finset.sum_range_succ']
85   simp only [Nat.add_zero, Nat.choose_zero_right, Nat.cast_one, mul_one]
86   rw [add_sub_cancel_right]
87   apply precision_sum
88   intro j _
89   apply precision_mul_nat
90   exact precision_mono (by norm_num) (H (1 + (j + 1)) (by omega))
91 
92 /-- The standard binomial denominator identity retains the valuation of the displacement. -/
93 lemma choose_precision (T k : ℕ) (hT : 0 < T) (hk : 0 < k) :
94     precision 2 ((padicValNat 2 T : ℤ) - Nat.log 2 k) (T.choose k : ℚ) := by
95   by_cases hzero : T.choose k = 0
96   · simp [hzero]
97   have hkT : k ≤ T := Nat.le_of_not_gt (by intro h; exact hzero (Nat.choose_eq_zero_of_lt h))
98   have hprev : (T - 1).choose (k - 1) ≠ 0 := Nat.ne_of_gt (Nat.choose_pos (by omega))
99   have hid : T * ((T - 1).choose (k - 1)) = T.choose k * k := by
100     simpa only [Nat.sub_add_cancel hT, Nat.sub_add_cancel hk] using
101       Nat.add_one_mul_choose_eq (T - 1) (k - 1)
102   have hv := congrArg (padicValNat 2) hid
103   rw [padicValNat.mul (by omega) hprev, padicValNat.mul hzero (by omega)] at hv
104   have hlog := padicValNat_le_nat_log (p := 2) k
105   apply Or.inr
106   rw [padicValRat.of_nat]
107   omega
108 
109 /-- Finite Gregory–Newton expansion, with its first two terms separated. -/
110 lemma displacement_expansion (f : ℕ → ℚ) (n T : ℕ) (hT : 0 < T) :
111     f (n + T) - f n = difference 1 1 f n * (T : ℚ) +
112       ∑ k ∈ Finset.range (T - 1), difference 1 (k + 2) f n * (T.choose (k + 2) : ℚ) := by
113   have hn := shift_eq_sum_fwdDiff_iter 1 f T n
114   simp only [nsmul_eq_mul, Nat.mul_one] at hn
115   change f (n + T) = ∑ k ∈ Finset.range (T + 1), (T.choose k : ℚ) * difference 1 k f n at hn
116   have ht : T + 1 = (T - 1) + 1 + 1 := by omega
117   rw [ht, Finset.sum_range_succ', Finset.sum_range_succ'] at hn
118   simp only [Nat.choose_zero_right, Nat.cast_one, difference_zero, one_mul,
119     Nat.zero_add, Nat.choose_one_right] at hn
120   rw [hn]
121   simp only [Nat.add_assoc, show 1 + 1 = 2 by rfl]
122   rw [show (∑ k ∈ Finset.range (T - 1), (T.choose (k + 2) : ℚ) * difference 1 (k + 2) f n) =
123       ∑ k ∈ Finset.range (T - 1), difference 1 (k + 2) f n * (T.choose (k + 2) : ℚ) by
124       apply Finset.sum_congr rfl; intro k _; ring]
125   ring
126 
127 /-- A strict Newton coefficient envelope gives the exact valuation of every displacement. -/
128 theorem exact_displacement (f : ℕ → ℚ) (c : ℕ)
129     (h1 : coefficient f 1 ≠ 0) (hv1 : padicValRat 2 (coefficient f 1) = (c : ℤ))
130     (H : ∀ k, 2 ≤ k → precision 2 ((c + 1 + Nat.log 2 k : ℕ) : ℤ) (coefficient f k))
131     (n T : ℕ) (hT : 0 < T) :
132     f (n + T) - f n ≠ 0 ∧
133       padicValRat 2 (f (n + T) - f n) = (padicValNat 2 T : ℤ) + (c : ℤ) := by
134   have hd := strict_dominance (coefficient f 1)
135     (difference 1 1 f n - coefficient f 1) (c : ℤ) h1 hv1 (first_difference_tail f c n H)
136   rw [add_sub_cancel] at hd
137   have hTq : (T : ℚ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hT)
138   have hvlead : padicValRat 2 (difference 1 1 f n * (T : ℚ)) =
139       (padicValNat 2 T : ℤ) + (c : ℤ) := by
140     rw [padicValRat.mul hd.1 hTq, hd.2, padicValRat.of_nat]
141     omega
142   rw [displacement_expansion f n T hT]
143   apply strict_dominance _ _ _ (mul_ne_zero hd.1 hTq) hvlead
144   apply precision_sum
145   intro k _
146   have hmul := precision_mul (translated_tail f c (k + 2) n (by omega) H)
147     (choose_precision T (k + 2) hT (by omega))
148   convert hmul using 1
149   push_cast
150   ring
151 
152 end KomorebiPaperIX.NewtonDominance

Back to source controls