ChargedDworkClosure.lean

1 module
2 public import CubicDworkClosure
3 @[expose] public section
4 noncomputable section
5 set_option autoImplicit false
6 namespace KomorebiPaperIX.ChargedDworkClosure
7 open DworkAlgebra
8 variable {K A : Type*} [Field K] [CommRing A] [Algebra K A]
9 
10 /-- A charged fourth derivative defect; multiplication adds its integer charge. -/
11 def B (D : Derivation K A A) (c : ℤ) : A →ₗ[K] A :=
12   (2:K)⁻¹ • (deriv D 4 - (c:K) • LinearMap.id)
13 
14 theorem B_deriv (D : Derivation K A A) (c : ℤ) (n : ℕ) (f : A) :
15     B D c (deriv D n f) = deriv D n (B D c f) := by
16   simp only [B, LinearMap.smul_apply, LinearMap.sub_apply, LinearMap.id_apply,
17     map_smul, map_sub, CubicDworkClosure.deriv_add]
18   rw [Nat.add_comm 4 n]
19 
20 theorem iterate_B_deriv (D : Derivation K A A) (c : ℤ) (s n : ℕ) (f : A) :
21     (B D c ^ s) (deriv D n f) = deriv D n ((B D c ^ s) f) := by
22   induction s with
23   | zero => rfl
24   | succ s ih => simp only [pow_succ', Module.End.mul_apply, ih, B_deriv]
25 
26 theorem B_mul [CharZero K] (D : Derivation K A A) (c d : ℤ) (f g : A) :
27     B D (c+d) (f*g) = B D c f*g + f*B D d g + middle D 2 4 f g := by
28   have h := prime_power_leibniz D 2 2 Nat.prime_two f g
29   norm_num only at h
30   simp only [B, LinearMap.smul_apply, LinearMap.sub_apply, LinearMap.id_apply]
31   rw [h]
32   simp only [Int.cast_add, Algebra.smul_def, map_add]
33   have hc := congrArg (algebraMap K A) (inv_mul_cancel₀ (by norm_num : (2:K)≠0))
34   simp only [map_mul, map_ofNat, map_one] at hc
35   linear_combination middle D 2 4 f g * hc
36 
37 @[simp] theorem B_zero_one (D : Derivation K A A) : B D 0 1 = 0 := by
38   simp [B, CubicDworkClosure.deriv_one_eq_zero D 4 (by decide)]
39 
40 def bounded (D : Derivation K A A) (c : ℤ) (I : Subring A) (n : ℕ) (f : A) : Prop :=
41   ∀ s ≤ n, (B D c ^ s) f ∈ I
42 
43 def flat (D : Derivation K A A) (c : ℤ) (I : Subring A) (f : A) : Prop :=
44   ∀ s, (B D c ^ s) f ∈ I
45 
46 @[simp] theorem bounded_zero (D : Derivation K A A) (c : ℤ) (I : Subring A) (f : A) :
47     bounded D c I 0 f ↔ f∈I := by simp [bounded]
48 
49 theorem bounded_mono (D : Derivation K A A) (c : ℤ) (I : Subring A) {n m : ℕ}
50     (h : m≤n) {f : A} (hf : bounded D c I n f) : bounded D c I m f :=
51   fun s hs => hf s (hs.trans h)
52 
53 theorem bounded_succ (D : Derivation K A A) (c : ℤ) (I : Subring A) (n : ℕ) (f : A) :
54     bounded D c I (n+1) f ↔ f∈I ∧ bounded D c I n (B D c f) := by
55   constructor
56   · intro hf
57     refine ⟨by simpa using hf 0 (by omega), ?_⟩
58     intro s hs
59     have h := hf (s+1) (by omega)
60     simpa only [pow_succ, Module.End.mul_apply] using h
61   · rintro ⟨hf,hb⟩ s hs
62     cases s with
63     | zero => simpa using hf
64     | succ s => simpa only [pow_succ, Module.End.mul_apply] using hb s (by omega)
65 
66 theorem bounded_add (D : Derivation K A A) (c : ℤ) (I : Subring A) (n : ℕ)
67     {f g : A} (hf : bounded D c I n f) (hg : bounded D c I n g) :
68     bounded D c I n (f+g) := by
69   intro s hs
70   rw [map_add]
71   exact I.add_mem (hf s hs) (hg s hs)
72 
73 theorem bounded_neg (D : Derivation K A A) (c : ℤ) (I : Subring A) (n : ℕ)
74     {f : A} (hf : bounded D c I n f) : bounded D c I n (-f) := by
75   intro s hs
76   rw [map_neg]
77   exact I.neg_mem (hf s hs)
78 
79 theorem bounded_sub (D : Derivation K A A) (c : ℤ) (I : Subring A) (n : ℕ)
80     {f g : A} (hf : bounded D c I n f) (hg : bounded D c I n g) :
81     bounded D c I n (f-g) := by
82   intro s hs
83   rw [map_sub]
84   exact I.sub_mem (hf s hs) (hg s hs)
85 
86 theorem bounded_nat_mul (D : Derivation K A A) (c : ℤ) (I : Subring A) (n a : ℕ)
87     {f : A} (hf : bounded D c I n f) : bounded D c I n ((a:A)*f) := by
88   intro s hs
89   rw [← nsmul_eq_mul, map_nsmul]
90   exact I.nsmul_mem (hf s hs) a
91 
92 theorem bounded_sum (D : Derivation K A A) (c : ℤ) (I : Subring A) (n : ℕ)
93     {ι : Type*} (S : Finset ι) (f : ι → A) (hf : ∀ i∈S, bounded D c I n (f i)) :
94     bounded D c I n (∑ i∈S, f i) := by
95   intro s hs
96   rw [map_sum]
97   exact I.sum_mem (fun i hi => hf i hi s hs)
98 
99 theorem bounded_deriv (D : Derivation K A A) (c : ℤ) (I : Subring A)
100     (hD : ∀ f∈I, D f∈I) (n a : ℕ) {f : A} (hf : bounded D c I n f) :
101     bounded D c I n (deriv D a f) := by
102   intro s hs
103   rw [iterate_B_deriv]
104   induction a with
105   | zero => exact hf s hs
106   | succ a ih => rw [deriv_succ]; exact hD _ ih
107 
108 theorem bounded_middle (D : Derivation K A A) (I : Subring A)
109     (hD : ∀ f∈I, D f∈I) (n : ℕ)
110     (hmul : ∀ c d f g, bounded D c I n f → bounded D d I n g → bounded D (c+d) I n (f*g))
111     (c d : ℤ) {f g : A} (hf : bounded D c I n f) (hg : bounded D d I n g) :
112     bounded D (c+d) I n (middle D 2 4 f g) := by
113   unfold middle
114   apply bounded_sum
115   intro k _
116   rw [mul_assoc]
117   apply bounded_nat_mul
118   exact hmul _ _ _ _ (bounded_deriv D c I hD n _ hf) (bounded_deriv D d I hD n _ hg)
119 
120 variable [CharZero K]
121 
122 /-- The all-order product theorem tracks additive charges. -/
123 theorem bounded_mul (D : Derivation K A A) (I : Subring A)
124     (hD : ∀ f∈I, D f∈I) (n : ℕ) (c d : ℤ) (f g : A)
125     (hf : bounded D c I n f) (hg : bounded D d I n g) : bounded D (c+d) I n (f*g) := by
126   induction n generalizing c d f g with
127   | zero => simpa using I.mul_mem ((bounded_zero D c I f).mp hf) ((bounded_zero D d I g).mp hg)
128   | succ n ih =>
129     have hfl := bounded_mono D c I (Nat.le_succ n) hf
130     have hgl := bounded_mono D d I (Nat.le_succ n) hg
131     rw [bounded_succ] at hf hg ⊢
132     refine ⟨I.mul_mem hf.1 hg.1, ?_⟩
133     rw [B_mul]
134     exact bounded_add D (c+d) I n
135       (bounded_add D (c+d) I n (ih _ _ _ _ hf.2 hgl) (ih _ _ _ _ hfl hg.2))
136       (bounded_middle D I hD n ih c d hfl hgl)
137 
138 theorem inverse_defect (D : Derivation K A A) (c : ℤ) (f g : A) (hfg : f*g=1) :
139     B D (-c) g = -(g*g*B D c f) - g*middle D 2 4 f g := by
140   have h := B_mul D c (-c) f g
141   rw [add_neg_cancel, hfg, B_zero_one] at h
142   linear_combination -g*h - (B D (-c) g)*hfg
143 
144 /-- Inverting an actual integral reciprocal negates the charge. -/
145 theorem bounded_inverse (D : Derivation K A A) (I : Subring A)
146     (hD : ∀ f∈I, D f∈I) (n : ℕ) (c : ℤ) (f g : A) (hfg : f*g=1)
147     (hf : bounded D c I n f) (hg : g∈I) : bounded D (-c) I n g := by
148   induction n with
149   | zero => simpa using hg
150   | succ n ih =>
151     have hfl := bounded_mono D c I (Nat.le_succ n) hf
152     have hgl := ih hfl
153     have hbf := (bounded_succ D c I n f).mp hf |>.2
154     rw [bounded_succ]
155     refine ⟨hg, ?_⟩
156     rw [inverse_defect D c f g hfg]
157     have hm := bounded_mul D I hD n
158     apply bounded_sub
159     · apply bounded_neg
160       have H := hm _ _ _ _ (hm _ _ _ _ hgl hgl) hbf
161       convert H using 1
162       omega
163     · have H := hm _ _ _ _ hgl (bounded_middle D I hD n hm c (-c) hfl hgl)
164       simpa only [add_neg_cancel, add_zero] using H
165 
166 theorem B_charge_shift (D : Derivation K A A) (c : ℤ) (f : A) :
167     B D (c+2) f = B D c f - f := by
168   simp only [B, LinearMap.smul_apply, LinearMap.sub_apply, LinearMap.id_apply]
169   simp only [Int.cast_add, Int.cast_ofNat, Algebra.smul_def, map_add, map_ofNat]
170   have hc := congrArg (algebraMap K A) (inv_mul_cancel₀ (by norm_num : (2:K)≠0))
171   simp only [map_mul, map_ofNat, map_one] at hc
172   linear_combination -f*hc
173 
174 theorem bounded_charge_shift (D : Derivation K A A) (c : ℤ) (I : Subring A)
175     (n : ℕ) (f : A) (hf : bounded D c I n f) : bounded D (c+2) I n f := by
176   induction n generalizing f with
177   | zero => simpa using hf
178   | succ n ih =>
179     have hfl := bounded_mono D c I (Nat.le_succ n) hf
180     rw [bounded_succ] at hf ⊢
181     refine ⟨hf.1, ?_⟩
182     rw [B_charge_shift]
183     exact bounded_sub D (c+2) I n (ih _ hf.2) (ih _ hfl)
184 
185 theorem flat_inverse (D : Derivation K A A) (I : Subring A)
186     (hD : ∀ f∈I, D f∈I) (c : ℤ) (f g : A) (hfg : f*g=1)
187     (hf : flat D c I f) (hg : g∈I) : flat D (-c) I g := by
188   intro s
189   exact bounded_inverse D I hD s c f g hfg (fun k _ => hf k) hg s le_rfl
190 
191 theorem flat_charge_shift (D : Derivation K A A) (c : ℤ) (I : Subring A)
192     (f : A) (hf : flat D c I f) : flat D (c+2) I f := by
193   intro s
194   exact bounded_charge_shift D c I s f (fun k _ => hf k) s le_rfl
195 
196 end KomorebiPaperIX.ChargedDworkClosure

Back to source controls