LogarithmTruncation.lean

1 import PaperX.LogarithmicRecovery
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Exponential and logarithm retain a supplied nilpotency bound
7 
8 The same annihilating exponent works before and after the finite exponential
9 or logarithm. In particular, logarithmic recovery can use the supplied bound
10 without calculating a new nilpotency class.
11 -/
12 
13 namespace PaperX.LogarithmTruncation
14 
15 open Finset PaperX.FiniteLogarithm
16 
17 variable {A : Type*} [Ring A] [Algebra ℚ A]
18 
19 /-- A polynomial without a constant term retains an annihilating exponent. -/
20 theorem sum_smul_pow_succ_pow_eq_zero {a : A} {d : ℕ} (ha : a ^ d = 0)
21     (s : Finset ℕ) (c : ℕ → ℚ) :
22     (∑ j ∈ s, c j • a ^ (j + 1)) ^ d = 0 := by
23   let b := ∑ j ∈ s, c j • a ^ j
24   have hab : Commute a b := by
25     exact Commute.sum_right _ _ _ fun j _ => ((Commute.refl a).pow_right j).smul_right _
26   have hfactor : (∑ j ∈ s, c j • a ^ (j + 1)) = a * b := by
27     simp only [b, mul_sum, mul_smul_comm, ← pow_succ']
28   rw [hfactor, hab.mul_pow, ha, zero_mul]
29 
30 /-- Passing from a nilpotent element to its unipotent exponential preserves
31 every supplied annihilating exponent. -/
32 theorem exp_sub_one_pow_eq_zero {a : A} {d : ℕ} (ha : a ^ d = 0) :
33     (IsNilpotent.exp a - 1) ^ d = 0 := by
34   nontriviality A
35   have hd : 0 < d := by
36     by_contra h
37     have hz : d = 0 := Nat.eq_zero_of_not_pos h
38     simp [hz] at ha
39   rw [IsNilpotent.exp_eq_sum ha, ← Nat.sub_add_cancel hd, Finset.sum_range_succ']
40   simp only [Nat.succ_eq_add_one, zero_add, Nat.factorial_zero, Nat.cast_one, inv_one,
41     pow_zero, one_smul, add_sub_cancel_right]
42   rw [Nat.sub_add_cancel hd]
43   exact sum_smul_pow_succ_pow_eq_zero ha _ _
44 
45 /-- Passing from a unipotent element to its logarithm preserves every supplied
46 annihilating exponent. -/
47 theorem log_pow_eq_zero {u : A} {d : ℕ} (hu : (u - 1) ^ d = 0) :
48     (log u) ^ d = 0 := by
49   nontriviality A
50   have hd : 0 < d := by
51     by_contra h
52     have hz : d = 0 := Nat.eq_zero_of_not_pos h
53     simp [hz] at hu
54   rw [log_eq_sum hu, ← Nat.sub_add_cancel hd, Finset.sum_range_succ']
55   simp only [Nat.succ_eq_add_one, Nat.cast_zero, div_zero, zero_smul, add_zero, zero_add]
56   rw [Nat.sub_add_cancel hd]
57   exact sum_smul_pow_succ_pow_eq_zero hu _ _
58 
59 /-- The inverse logarithm may be truncated at the original nilpotency bound. -/
60 theorem log_exp_eq_sum {a : A} {d : ℕ} (ha : a ^ d = 0) :
61     (∑ j ∈ range d, ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) •
62       (IsNilpotent.exp a - 1) ^ j) = a := by
63   rw [← log_eq_sum (exp_sub_one_pow_eq_zero ha)]
64   exact PaperX.NilpotentLogarithm.log_exp ⟨d, ha⟩
65 
66 /-- The exponential preserves the complete collection of annihilating exponents. -/
67 theorem exp_sub_one_pow_eq_zero_iff {a : A} (ha : IsNilpotent a) (d : ℕ) :
68     (IsNilpotent.exp a - 1) ^ d = 0 ↔ a ^ d = 0 := by
69   constructor
70   · intro h
71     simpa only [PaperX.NilpotentLogarithm.log_exp ha] using log_pow_eq_zero h
72   · exact exp_sub_one_pow_eq_zero
73 
74 /-- The logarithm preserves the complete collection of annihilating exponents. -/
75 theorem log_pow_eq_zero_iff {u : A} (hu : IsNilpotent (u - 1)) (d : ℕ) :
76     (log u) ^ d = 0 ↔ (u - 1) ^ d = 0 := by
77   constructor
78   · intro h
79     simpa only [PaperX.NilpotentLogarithm.exp_log hu] using exp_sub_one_pow_eq_zero h
80   · exact log_pow_eq_zero
81 
82 /-- The nilpotency class is unchanged by the exponential minus the identity. -/
83 theorem nilpotencyClass_exp_sub_one {a : A} (ha : IsNilpotent a) :
84     nilpotencyClass (IsNilpotent.exp a - 1) = nilpotencyClass a := by
85   apply congrArg sInf
86   ext d
87   exact exp_sub_one_pow_eq_zero_iff ha d
88 
89 /-- The nilpotency class is unchanged by the finite logarithm. -/
90 theorem nilpotencyClass_log {u : A} (hu : IsNilpotent (u - 1)) :
91     nilpotencyClass (log u) = nilpotencyClass (u - 1) := by
92   apply congrArg sInf
93   ext d
94   exact log_pow_eq_zero_iff hu d
95 
96 section CoefficientField
97 
98 variable {K V : Type*} [Field K] [CharZero K] [AddCommGroup V] [Module K V]
99 
100 local instance : Algebra ℚ (Module.End K V) :=
101   Algebra.compHom (Module.End K V) (algebraMap ℚ K)
102 
103 /-- A supplied monodromy bound gives an explicit recovery polynomial over
104 the original coefficient field, with precisely that cutoff. -/
105 theorem monodromy_eq_log_sum {N : Module.End K V} {d : ℕ} (hN : N ^ d = 0)
106     {t : K} (ht : t ≠ 0) :
107     N = t⁻¹ • ∑ j ∈ range d, ((-1 : K) ^ (j + 1) / (j : K)) •
108       (PaperX.NilpotentExponential.expN N t - 1) ^ j := by
109   have htN : (t • N) ^ d = 0 := by rw [smul_pow, hN, smul_zero]
110   have hU : (PaperX.NilpotentExponential.expN N t - 1) ^ d = 0 :=
111     exp_sub_one_pow_eq_zero htN
112   calc
113     N = PaperX.LogarithmicRecovery.recoverN t (PaperX.NilpotentExponential.expN N t) :=
114       (PaperX.LogarithmicRecovery.recoverN_expN ⟨d, hN⟩ ht).symm
115     _ = _ := by
116       rw [PaperX.LogarithmicRecovery.recoverN, PaperX.LogarithmicRecovery.log_polynomial hU]
117 
118 end CoefficientField
119 
120 end PaperX.LogarithmTruncation

Back to source controls