The principal declarations in this module are:
geomSeriesThe geometric series element is the finite sum of successive powers.
geomSeries_eq_sum_powThe geometric series equals the finite sum of powers.
geomSeries_zeroThe geometric series of length zero is zero.
geomSeries_oneThe geometric series of length one is one.
The geometric series element is the finite sum of successive powers.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialdef geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
FoxDifferential.GroupRing AThe geometric series equals the finite sum of powers.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_eq_sum_pow {A : Type*} [Group A] (a : A) (n : ℕ) :
geomSeries a n = ∑ k ∈ Finset.range n,
(MonoidAlgebra.of ℤ A a : FoxDifferential.GroupRing A) ^ kThe geometric series of length zero is zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_zero {A : Type*} [Group A] (a : A) :
geomSeries a 0 = 0The geometric series of length one is one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_one {A : Type*} [Group A] (a : A) :
geomSeries a 1 = 1The augmentation map has the stated value on group-ring elements.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem augmentation_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
FoxDifferential.augmentation A (geomSeries a n) = nThe geometric series is nonzero when the natural length is nonzero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_ne_zero_of_nat_ne_zero {A : Type*} [Group A]
(a : A) {n : ℕ} (hn : n ≠ 0) :
geomSeries a n ≠ 0The successor geometric series is obtained by adding the last power.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_succ_eq_add_pow {A : Type*} [Group A] (a : A) (n : ℕ) :
geomSeries a (n + 1) =
geomSeries a n + MonoidAlgebra.of ℤ A (a ^ n)The geometric series for a sum of lengths splits into the initial series plus the shifted tail series.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_add {A : Type*} [CommGroup A] (a : A) (m n : ℕ) :
geomSeries a (m + n) =
geomSeries a m + MonoidAlgebra.of ℤ A (a ^ m) * geomSeries a nThe successor geometric series satisfies the multiplicative recurrence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem geomSeries_succ_eq_mul_add_one {A : Type*} [Group A] (a : A) (n : ℕ) :
geomSeries a (n + 1) =
geomSeries a n * MonoidAlgebra.of ℤ A a + 1The difference \(1 - x^n\) factors as \((1 - x)\) times the geometric series.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem one_sub_pow_eq_one_sub_mul_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
(1 - MonoidAlgebra.of ℤ A (a ^ n) : FoxDifferential.GroupRing A) =
(1 - MonoidAlgebra.of ℤ A a) * geomSeries a nThe difference \(x^n - 1\) factors as \((x - 1)\) times the geometric series.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferentialtheorem pow_sub_one_eq_sub_one_mul_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
(MonoidAlgebra.of ℤ A (a ^ n) - 1 : FoxDifferential.GroupRing A) =
(MonoidAlgebra.of ℤ A a - 1) * geomSeries a n