DyadicFourAllRows.lean

1 module
2 public import ChargedDworkClosure
3 public import DyadicFourCongruences
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace KomorebiPaperIX.DyadicFourAllRows
8 open PowerSeries DworkAlgebra HurwitzDworkClosure DworkCriterion Mahler
9 open DyadicFourKernel DyadicFourDwork DyadicFourCongruences
10 
11 abbrev B : PowerSeries ℚ_[2] →ₗ[ℚ_[2]] PowerSeries ℚ_[2] :=
12   ChargedDworkClosure.B (derivative ℚ_[2]) 1
13 
14 def Flat (f : PowerSeries ℚ_[2]) : Prop :=
15   ChargedDworkClosure.flat (derivative ℚ_[2]) 1 (integralSeries 2) f
16 
17 def CoeffFlat (a : ℕ→ℤ_[2]) : Prop := ∀s d, (2:ℤ_[2])^s ∣ difference 4 s a d
18 
19 theorem decode_B (f : PowerSeries ℚ_[2]) (d : ℕ) :
20     EGF.decode (B f) d = (2:ℚ_[2])⁻¹*(EGF.decode f (d+4)-EGF.decode f d) := by
21   simp only [B,ChargedDworkClosure.B,LinearMap.smul_apply,LinearMap.sub_apply,
22     LinearMap.id_apply,Int.cast_one,one_smul]
23   simp only [EGF.decode,coeff_smul,map_sub,smul_eq_mul]
24   have h4 := decode_deriv 2 f 4 d
25   simp only [EGF.decode] at h4
26   linear_combination (2:ℚ_[2])⁻¹*h4
27 
28 theorem decode_B_iter (f : PowerSeries ℚ_[2]) (s d : ℕ) :
29     EGF.decode ((B^s) f) d = ((2:ℚ_[2])⁻¹)^s*difference 4 s (EGF.decode f) d := by
30   induction s generalizing d with
31   | zero => simp
32   | succ s ih =>
33     rw [pow_succ',Module.End.mul_apply,decode_B,ih,ih,difference_succ,pow_succ]
34     ring
35 
36 theorem difference_coe (a : ℕ→ℤ_[2]) (s d : ℕ) :
37     difference 4 s (fun n => (a n:ℚ_[2])) d = ((difference 4 s a d:ℤ_[2]):ℚ_[2]) := by
38   induction s generalizing d with
39   | zero => rfl
40   | succ s ih => rw [difference_succ,difference_succ,ih,ih]; rfl
41 
42 theorem flat_encode_iff (a : ℕ→ℤ_[2]) : Flat (encodeIntegral 2 a) ↔ CoeffFlat a := by
43   have he : EGF.decode (encodeIntegral 2 a) = fun n => (a n:ℚ_[2]) := by
44     funext n; exact decode_encodeIntegral 2 a n
45   constructor
46   · intro H s d
47     have hd := H s d
48     change EGF.decode ((B^s) (encodeIntegral 2 a)) d ∈ _ at hd
49     rw [decode_B_iter,he,difference_coe] at hd
50     exact (normalized_mem_iff 2 _ s).mp hd
51   · intro H s d
52     change EGF.decode ((B^s) (encodeIntegral 2 a)) d ∈ _
53     rw [decode_B_iter,he,difference_coe]
54     exact (normalized_mem_iff 2 _ s).mpr (H s d)
55 
56 theorem packed_difference_support (a : ℕ→ℤ_[2]) (s d : ℕ) (hd : ¬4∣d) :
57     difference 4 s (packed 4 a) d = 0 := by
58   induction s generalizing d with
59   | zero => simp [packed,hd]
60   | succ s ih =>
61     have hd4 : ¬4∣d+4 := by simpa using hd
62     rw [difference_succ,ih _ hd4,ih _ hd,sub_self]
63 
64 theorem packed_flat_of_kummer (a : ℕ→ℤ_[2]) (H : KummerSequences.Kummer 2 a) :
65     CoeffFlat (packed 4 a) := by
66   intro s d
67   by_cases hd : 4∣d
68   · obtain ⟨r,rfl⟩ := hd
69     change (2:ℤ_[2])^s ∣ difference (4*1) s (packed 4 a) (4*r)
70     rw [packet_difference 4 1 s r (by decide)]
71     exact H s r
72   · rw [packed_difference_support a s d hd]
73     exact dvd_zero _
74 
75 theorem source_flat (j : ℕ) : Flat (sourceSeries j) :=
76   (flat_encode_iff _).mpr (packed_flat_of_kummer _ (source_kummer j))
77 
78 /-- Reciprocal closure for the unshifted fourth-order operator is derived with charges. -/
79 theorem flat_reciprocal (f : PowerSeries ℚ_[2]) (H : Flat f) (h0 : constantCoeff f=1) :
80     Flat f⁻¹ := by
81   have hi := ChargedDworkClosure.flat_inverse (derivative ℚ_[2])
82     (integralSeries 2) (integral_derivative 2) 1 f f⁻¹
83     (PowerSeries.mul_inv_cancel f (by rw [h0]; exact one_ne_zero)) H
84     (integral_inverse 2 f (H 0) h0)
85   have hs := ChargedDworkClosure.flat_charge_shift (derivative ℚ_[2]) (-1)
86     (integralSeries 2) f⁻¹ hi
87   exact hs
88 
89 theorem actual_packet_flat (j : ℕ) (hj : j<4) :
90     Flat (PowerSeries.map (Rat.castHom ℚ_[2])
91       (ExponentialSection.expandedPacket 4 (by decide) j)) := by
92   rw [packet_is_reciprocal j hj]
93   exact flat_reciprocal _ (source_flat j) (sourceSeries_constant j hj)
94 
95 theorem lifted_flat (j : ℕ) (hj : j<4) : CoeffFlat (packed 4 (normalizedLift j hj)) := by
96   apply (flat_encode_iff _).mp
97   rw [normalizedLift,SeriesDifferenceBridge.packet_encoding 2 4 _ _ (packet_support j)]
98   exact actual_packet_flat j hj
99 
100 /-- Full normalized Kummer divisibility at every row, including n=0. -/
101 theorem base_step_bound (j k n : ℕ) (hj : j<4) :
102     (2:ℤ_[2])^k ∣ difference 1 k (normalizedLift j hj) n := by
103   have H := lifted_flat j hj k (4*n)
104   change (2:ℤ_[2])^k ∣ difference (4*1) k (packed 4 (normalizedLift j hj)) (4*n) at H
105   rw [packet_difference 4 1 k n (by decide)] at H
106   exact H
107 
108 /-- Every natural-number step inherits the full order, uniformly from the first row. -/
109 theorem normalized_bound (j u k n : ℕ) (hj : j<4) :
110     (2:ℤ_[2])^k ∣ difference u k (normalizedLift j hj) n := by
111   have H := StepMultiples.divisibility_transfer ((2:ℤ_[2])^k) 1 u k 0
112     (normalizedLift j hj) (fun r _ => base_step_bound j k r hj) n (Nat.zero_le n)
113   simpa only [mul_one] using H
114 
115 theorem normalized_precision (j u k n : ℕ) (hj : j<4) :
116     GlobalEulerBoundary.precision 2 (k:ℤ)
117       (difference u k (Congruential.coeff 4 j) n) :=
118   StandardWindowPrecision.rational_precision_of_divisibility 2
119     (difference u k (normalizedLift j hj) n) _ (normalized_difference_coe j u k n hj)
120     _ (normalized_bound j u k n hj)
121 
122 theorem unnormalized_bound (j u k n : ℕ) (hj : j<4) :
123     (2:ℤ_[2])^k ∣ difference u k (unnormalizedLift j hj) n := by
124   have he : difference u k (unnormalizedLift j hj) n =
125       (j.factorial:ℤ_[2])*difference u k (normalizedLift j hj) n := by
126     induction k generalizing n with
127     | zero => rfl
128     | succ k ih => rw [difference_succ,ih,ih,difference_succ,mul_sub]
129   rw [he]
130   exact dvd_mul_of_dvd_right (normalized_bound j u k n hj) _
131 
132 theorem unnormalized_precision (j u k n : ℕ) (hj : j<4) :
133     GlobalEulerBoundary.precision 2 (k:ℤ)
134       (difference u k (Congruential.unnormalized 4 j) n) :=
135   StandardWindowPrecision.rational_precision_of_divisibility 2
136     (difference u k (unnormalizedLift j hj) n) _ (unnormalized_difference_coe j u k n hj)
137     _ (unnormalized_bound j u k n hj)
138 
139 end KomorebiPaperIX.DyadicFourAllRows

Back to source controls