StepAmplification.lean

1 module
2 public import PeriodFromDifferences
3 public import DifferenceStepMultiples
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace KomorebiPaperIX.StepAmplification
8 open Mahler
9 variable (p : ℕ) [Fact p.Prime]
10 
11 /-- Positive Newton coefficients supply the valuation of the displacement multiplier. -/
12 theorem binomial_step_precision (u a : ℕ) (ha : 0<a) (hau : a≤u) :
13     p^(padicValNat p u+1) ∣ u.choose a * p^a := by
14   have hp : p.Prime := Fact.out
15   have hu : 0<u := lt_of_lt_of_le ha hau
16   have hc : u.choose a ≠ 0 := Nat.choose_ne_zero hau
17   have he := Nat.add_one_mul_choose_eq (u-1) (a-1)
18   rw [Nat.sub_add_cancel (by omega : 1≤u), Nat.sub_add_cancel (by omega : 1≤a)] at he
19   have hd : p^(padicValNat p u) ∣ u.choose a * a := by
20     rw [←he]
21     exact dvd_mul_of_dvd_left (pow_padicValNat_dvd) _
22   have hv := (padicValNat_dvd_iff_le (Nat.mul_ne_zero hc ha.ne')).mp hd
23   rw [padicValNat.mul hc ha.ne'] at hv
24   have hva := PeriodFromDifferences.valuation_lt p a ha
25   apply (padicValNat_dvd_iff_le (Nat.mul_ne_zero hc (pow_ne_zero _ hp.ne_zero))).mpr
26   rw [padicValNat.mul hc (pow_ne_zero _ hp.ne_zero), padicValNat.prime_pow]
27   omega
28 
29 variable {R : Type*} [CommRing R]
30 
31 /-- A displacement consumes base differences and adds its valuation to their first-order gain.
32 The cap M is fixed at the inspected row. No period hypothesis is used. -/
33 theorem offset_displacement (f : ℕ→R) (h n u A M : ℕ)
34     (H : ∀ a, (p:R)^(min (A+a) M) ∣ difference h a f n) :
35     (p:R)^(min (A+padicValNat p u+1) M) ∣ f (n+u*h)-f n := by
36   rw [PeriodFromDifferences.displacement_expansion]
37   apply Finset.dvd_sum
38   intro a ha
39   have hau : a+1≤u := by have := Finset.mem_range.mp ha; omega
40   by_cases hs : A+(a+1)<M
41   · have hd := H (a+1)
42     rw [min_eq_left (Nat.le_of_lt hs)] at hd
43     obtain ⟨b,hb⟩ := hd
44     rw [hb]
45     have hn := binomial_step_precision p u (a+1) (by omega) hau
46     have hc : (p:R)^(padicValNat p u+1) ∣ (u.choose (a+1):R)*(p:R)^(a+1) := by
47       obtain ⟨c,hc⟩ := hn
48       refine ⟨(c:R), ?_⟩
49       simpa only [Nat.cast_mul,Nat.cast_pow] using congrArg (fun x:ℕ => (x:R)) hc
50     have hpA : (p:R)^(A+(padicValNat p u+1)) ∣
51         (u.choose (a+1):R)*((p:R)^(A+(a+1))*b) := by
52       obtain ⟨c,hc⟩ := hc
53       refine ⟨c*b, ?_⟩
54       calc
55         _ = (p:R)^A * ((u.choose (a+1):R)*(p:R)^(a+1))*b := by rw [pow_add]; ring
56         _ = (p:R)^A * ((p:R)^(padicValNat p u+1)*c)*b := by rw [hc]
57         _ = _ := by rw [pow_add]; ring
58     apply dvd_trans (pow_dvd_pow (p:R) (min_le_left _ _))
59     simpa only [Nat.add_assoc] using hpA
60   · have hd := H (a+1)
61     rw [min_eq_right (by omega : M≤A+(a+1))] at hd
62     exact dvd_trans (pow_dvd_pow (p:R) (min_le_right _ _)) (dvd_mul_of_dvd_right hd _)
63 
64 /-- Difference composition is iteration of the same operator. -/
65 theorem difference_compose (h a b : ℕ) (f : ℕ→R) :
66     difference h a (difference h b f)=difference h (a+b) f := by
67   simp only [difference,Function.iterate_add_apply]
68 
69 /-- Repeated displacement, while retaining every base-difference offset. -/
70 theorem repeated_offset (f : ℕ→R) (h n u M : ℕ)
71     (H : ∀ a, (p:R)^(min a M) ∣ difference h a f n) (k a : ℕ) :
72     (p:R)^(min (k*(padicValNat p u+1)+a) M) ∣
73       difference h a (difference (u*h) k f) n := by
74   induction k generalizing a with
75   | zero => simpa using H a
76   | succ k ih =>
77     have he : difference (u*h) (k+1) f = difference (u*h) 1 (difference (u*h) k f) := by
78       rw [difference_compose]; congr 1; omega
79     rw [he,StepMultiples.difference_commute_one,difference_one]
80     have hd := offset_displacement p (difference h a (difference (u*h) k f)) h n u
81       (k*(padicValNat p u+1)+a) M (by
82         intro b
83         rw [difference_compose]
84         simpa only [Nat.add_assoc,Nat.add_comm a b] using ih (a+b))
85     simpa only [Nat.succ_mul,Nat.add_assoc,Nat.add_left_comm,Nat.add_comm] using hd
86 
87 /-- Any natural multiplier: zero step is included because its positive differences vanish. -/
88 theorem repeated_precision (f : ℕ→R) (h n u M : ℕ)
89     (H : ∀ a, (p:R)^(min a M) ∣ difference h a f n) (k : ℕ) :
90     (p:R)^(min (k*(padicValNat p u+1)) M) ∣ difference (u*h) k f n := by
91   simpa only [Nat.add_zero,difference_zero] using repeated_offset p f h n u M H k 0
92 
93 end KomorebiPaperIX.StepAmplification

Back to source controls