Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.RightDerivative.GeometricSeries
ProCGroups/FoxDifferential/RightDerivative/GeometricSeries

ProCGroups.FoxDifferential.RightDerivative.GeometricSeries

10 Theorems | 1 Definition

The principal declarations in this module are:

  • geomSeries The geometric series element is the finite sum of successive powers. - geomSeries_eq_sum_pow The geometric series equals the finite sum of powers. - geomSeries_zero The geometric series of length zero is zero. - geomSeries_one The geometric series of length one is one.
imports
Imported by

Declarations

Definition FoxDifferential.geomSeries 
noncomputable def geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
    FoxDifferential.GroupRing A :=
  ∑ k ∈ Finset.range n, MonoidAlgebra.of ℤ A (a ^ k)

The geometric series element is the finite sum of successive powers.

Theorem FoxDifferential.geomSeries_eq_sum_pow 
theorem 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) ^ k

The geometric series equals the finite sum of powers.

Show Lean proof
Theorem FoxDifferential.geomSeries_zero 
@[simp]
theorem geomSeries_zero {A : Type*} [Group A] (a : A) :
    geomSeries a 0 = 0

The geometric series of length zero is zero.

Show Lean proof
Theorem FoxDifferential.geomSeries_one 
@[simp]
theorem geomSeries_one {A : Type*} [Group A] (a : A) :
    geomSeries a 1 = 1

The geometric series of length one is one.

Show Lean proof
Theorem FoxDifferential.augmentation_geomSeries 
@[simp]
theorem augmentation_geomSeries {A : Type*} [Group A] (a : A) (n : ℕ) :
    FoxDifferential.augmentation A (geomSeries a n) = n

The augmentation map has the stated value on group-ring elements.

Show Lean proof
Theorem FoxDifferential.geomSeries_ne_zero_of_nat_ne_zero 
theorem geomSeries_ne_zero_of_nat_ne_zero {A : Type*} [Group A]
    (a : A) {n : ℕ} (hn : n ≠ 0) :
    geomSeries a n ≠ 0

The geometric series is nonzero when the natural length is nonzero.

Show Lean proof
Theorem FoxDifferential.geomSeries_succ_eq_add_pow 
theorem 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 successor geometric series is obtained by adding the last power.

Show Lean proof
Theorem FoxDifferential.geomSeries_add 
theorem geomSeries_add {A : Type*} [CommGroup A] (a : A) (m n : ℕ) :
    geomSeries a (m + n) =
      geomSeries a m + MonoidAlgebra.of ℤ A (a ^ m) * geomSeries a n

The geometric series for a sum of lengths splits into the initial series plus the shifted tail series.

Show Lean proof
Theorem FoxDifferential.geomSeries_succ_eq_mul_add_one 
theorem geomSeries_succ_eq_mul_add_one {A : Type*} [Group A] (a : A) (n : ℕ) :
    geomSeries a (n + 1) =
      geomSeries a n * MonoidAlgebra.of ℤ A a + 1

The successor geometric series satisfies the multiplicative recurrence.

Show Lean proof
Theorem FoxDifferential.one_sub_pow_eq_one_sub_mul_geomSeries 
theorem 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 n

The difference \(1 - x^n\) factors as \((1 - x)\) times the geometric series.

Show Lean proof
Theorem FoxDifferential.pow_sub_one_eq_sub_one_mul_geomSeries 
theorem 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

The difference \(x^n - 1\) factors as \((x - 1)\) times the geometric series.

Show Lean proof