FoxDifferential/RightDerivative/GeometricSeries.lean
1import FoxDifferential.Discrete.GroupRing
2import Mathlib.Algebra.Ring.GeomSum
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/RightDerivative/GeometricSeries.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Right Fox derivatives
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable def geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
21 ∑ k ∈ Finset.range n, MonoidAlgebra.of ℤ A (a ^ k)
23theorem geomSeries_eq_sum_pow {A : Type*} [Group A] (a : A) (n : ℕ) :
24 geomSeries a n = ∑ k ∈ Finset.range n,
25 (MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) ^ k := by
26 simp only [geomSeries, map_pow, MonoidAlgebra.of_apply, MonoidAlgebra.single_pow, one_pow]
28@[simp]
29theorem geomSeries_zero {A : Type*} [Group A] (a : A) :
30 geomSeries a 0 = 0 := by
31 simp only [geomSeries, Finset.range_zero, MonoidAlgebra.of_apply, Finset.sum_empty]
33@[simp]
34theorem geomSeries_one {A : Type*} [Group A] (a : A) :
35 geomSeries a 1 = 1 := by
36 simpa [geomSeries] using (FoxDifferential.groupRing_of_one (H := A))
38@[simp]
39theorem augmentation_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
40 FoxDifferential.augmentation A (geomSeries a n) = n := by
41 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, geomSeries, MonoidAlgebra.of_apply,
42 map_sum, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one,
43 Finset.sum_const, Finset.card_range, Int.nsmul_eq_mul]
45theorem geomSeries_ne_zero_of_nat_ne_zero {A : Type*} [Group A]
46 (a : A) {n : ℕ} (hn : n ≠ 0) :
47 geomSeries a n ≠ 0 := by
48 intro hzero
49 have haug := congrArg (FoxDifferential.augmentation A) hzero
50 rw [augmentation_geomSeries] at haug
52 exact hn haug
54theorem geomSeries_succ_eq_add_pow {A : Type*} [Group A] (a : A) (n : ℕ) :
55 geomSeries a (n + 1) =
56 geomSeries a n + MonoidAlgebra.of ℤ A (a ^ n) := by
57 simp only [geomSeries, Finset.range_add_one, MonoidAlgebra.of_apply, Finset.mem_range, lt_self_iff_false,
58 not_false_eq_true, Finset.sum_insert, add_comm]
60theorem geomSeries_add {A : Type*} [CommGroup A] (a : A) (m n : ℕ) :
61 geomSeries a (m + n) =
62 geomSeries a m + MonoidAlgebra.of ℤ A (a ^ m) * geomSeries a n := by
63 induction n with
65 simp only [add_zero, MonoidAlgebra.of_apply, geomSeries_zero, mul_zero]
66 | succ n ih =>
67 rw [Nat.add_succ, geomSeries_succ_eq_add_pow, ih, geomSeries_succ_eq_add_pow]
68 rw [mul_add]
69 simp only [MonoidAlgebra.of_apply, pow_add, MonoidAlgebra.single_mul_single, mul_one]
70 ring
72theorem geomSeries_succ_eq_mul_add_one {A : Type*} [Group A] (a : A) (n : ℕ) :
73 geomSeries a (n + 1) =
74 geomSeries a n * MonoidAlgebra.of ℤ A a + 1 := by
76 let x : FoxDifferential.GroupRing A := MonoidAlgebra.of ℤ A a
77 have h := geom_sum_succ (x := MulOpposite.op x) (n := n)
78 have h2 := congrArg MulOpposite.unop h
79 dsimp [x] at h2
80 simpa using h2
82theorem one_sub_pow_eq_one_sub_mul_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
83 (1 - MonoidAlgebra.of ℤ A (a ^ n) : FoxDifferential.GroupRing A) =
84 (1 - MonoidAlgebra.of ℤ A a) * geomSeries a n := by
85 rw [geomSeries_eq_sum_pow]
86 simpa [map_pow] using
87 (mul_neg_geom_sum (MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) n).symm
89theorem pow_sub_one_eq_sub_one_mul_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
90 (MonoidAlgebra.of ℤ A (a ^ n) - 1 : FoxDifferential.GroupRing A) =
91 (MonoidAlgebra.of ℤ A a - 1) * geomSeries a n := by
92 rw [geomSeries_eq_sum_pow]
93 simpa [map_pow] using
94 (mul_geom_sum (MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) n).symm
96end FoxDifferential