Source: ProCGroups.FoxDifferential.RightDerivative.GeometricSeries
1import ProCGroups.FoxDifferential.Discrete.GroupRing
2import Mathlib.Algebra.Ring.GeomSum
4/-!
5# Fox differential: right derivative — geometric series
7The principal declarations in this module are:
9- `geomSeries`
10 The geometric series element is the finite sum of successive powers.
11- `geomSeries_eq_sum_pow`
12 The geometric series equals the finite sum of powers.
13- `geomSeries_zero`
14 The geometric series of length zero is zero.
15- `geomSeries_one`
16 The geometric series of length one is one.
17-/
19namespace FoxDifferential
21/-- The geometric series element is the finite sum of successive powers. -/
22noncomputable def geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
24 ∑ k ∈ Finset.range n, MonoidAlgebra.of ℤ A (a ^ k)
26/-- The geometric series equals the finite sum of powers. -/
27theorem geomSeries_eq_sum_pow {A : Type*} [Group A] (a : A) (n : ℕ) :
28 geomSeries a n = ∑ k ∈ Finset.range n,
29 (MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) ^ k := by
30 simp only [geomSeries, map_pow, MonoidAlgebra.of_apply, MonoidAlgebra.single_pow, one_pow]
32/-- The geometric series of length zero is zero. -/
33@[simp]
34theorem geomSeries_zero {A : Type*} [Group A] (a : A) :
35 geomSeries a 0 = 0 := by
36 simp only [geomSeries, Finset.range_zero, MonoidAlgebra.of_apply, Finset.sum_empty]
38/-- The geometric series of length one is one. -/
39@[simp]
40theorem geomSeries_one {A : Type*} [Group A] (a : A) :
41 geomSeries a 1 = 1 := by
42 simpa [geomSeries] using (FoxDifferential.groupRing_of_one (H := A))
44/-- The augmentation map has the stated value on group-ring elements. -/
45@[simp]
46theorem augmentation_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
47 FoxDifferential.augmentation A (geomSeries a n) = n := by
48 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, geomSeries,
49 MonoidAlgebra.of_apply,
50 map_sum, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul,
51 mul_one,
52 Finset.sum_const, Finset.card_range, Int.nsmul_eq_mul]
54/-- The geometric series is nonzero when the natural length is nonzero. -/
55theorem geomSeries_ne_zero_of_nat_ne_zero {A : Type*} [Group A]
56 (a : A) {n : ℕ} (hn : n ≠ 0) :
57 geomSeries a n ≠ 0 := by
58 intro hzero
59 have haug := congrArg (FoxDifferential.augmentation A) hzero
60 rw [augmentation_geomSeries] at haug
61 simp only [map_zero, Int.natCast_eq_zero] at haug
62 exact hn haug
64/-- The successor geometric series is obtained by adding the last power. -/
65theorem geomSeries_succ_eq_add_pow {A : Type*} [Group A] (a : A) (n : ℕ) :
66 geomSeries a (n + 1) =
67 geomSeries a n + MonoidAlgebra.of ℤ A (a ^ n) := by
68 simp only [geomSeries, Finset.range_add_one, MonoidAlgebra.of_apply, Finset.mem_range,
69 lt_self_iff_false,
70 not_false_eq_true, Finset.sum_insert, add_comm]
72/--
73The geometric series for a sum of lengths splits into the initial series plus the shifted tail
74series.
75-/
76theorem geomSeries_add {A : Type*} [CommGroup A] (a : A) (m n : ℕ) :
77 geomSeries a (m + n) =
78 geomSeries a m + MonoidAlgebra.of ℤ A (a ^ m) * geomSeries a n := by
79 induction n with
80 | zero =>
81 simp only [add_zero, MonoidAlgebra.of_apply, geomSeries_zero, mul_zero]
82 | succ n ih =>
83 rw [Nat.add_succ, geomSeries_succ_eq_add_pow, ih, geomSeries_succ_eq_add_pow]
84 rw [mul_add]
85 simp only [MonoidAlgebra.of_apply, pow_add, MonoidAlgebra.single_mul_single, mul_one]
86 ring
88/-- The successor geometric series satisfies the multiplicative recurrence. -/
89theorem geomSeries_succ_eq_mul_add_one {A : Type*} [Group A] (a : A) (n : ℕ) :
90 geomSeries a (n + 1) =
91 geomSeries a n * MonoidAlgebra.of ℤ A a + 1 := by
92 rw [geomSeries_eq_sum_pow, geomSeries_eq_sum_pow]
93 let x : FoxDifferential.GroupRing A := MonoidAlgebra.of ℤ A a
94 have h := geom_sum_succ (x := MulOpposite.op x) (n := n)
95 have h2 := congrArg MulOpposite.unop h
96 dsimp [x] at h2
97 simpa using h2
99/-- The difference \(1 - x^n\) factors as \((1 - x)\) times the geometric series. -/
100theorem one_sub_pow_eq_one_sub_mul_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
101 (1 - MonoidAlgebra.of ℤ A (a ^ n) : FoxDifferential.GroupRing A) =
102 (1 - MonoidAlgebra.of ℤ A a) * geomSeries a n := by
103 rw [geomSeries_eq_sum_pow]
104 simpa [map_pow] using
105 (mul_neg_geom_sum (MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) n).symm
107/-- The difference \(x^n - 1\) factors as \((x - 1)\) times the geometric series. -/
108theorem pow_sub_one_eq_sub_one_mul_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
109 (MonoidAlgebra.of ℤ A (a ^ n) - 1 : FoxDifferential.GroupRing A) =
110 (MonoidAlgebra.of ℤ A a - 1) * geomSeries a n := by
111 rw [geomSeries_eq_sum_pow]
112 simpa [map_pow] using
113 (mul_geom_sum (MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) n).symm
115end FoxDifferential