feat(RingTheory): geometric series of (Mv)PowerSeries (#30599)

Also abstracted the common part for both PowerSeries and normed rings into `Summable.tsum_pow_mul_one_sub` / `Summable.one_sub_mul_tsum_pow`.

Author: wwylele

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -304,21 +304,11 @@ theorem tsum_geometric_le_of_norm_lt_one (x : R) (h : ‖x‖ < 1) :
 
 variable [HasSummableGeomSeries R]
 
-theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * (1 - x) = 1 := by
-  have := (summable_geometric_of_norm_lt_one h).hasSum.mul_right (1 - x)
-  refine tendsto_nhds_unique this.tendsto_sum_nat ?_
-  have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
-    simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)
-  convert← this
-  rw [← geom_sum_mul_neg, Finset.sum_mul]
-
-theorem mul_neg_geom_series (x : R) (h : ‖x‖ < 1) : (1 - x) * ∑' i : ℕ, x ^ i = 1 := by
-  have := (summable_geometric_of_norm_lt_one h).hasSum.mul_left (1 - x)
-  refine tendsto_nhds_unique this.tendsto_sum_nat ?_
-  have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
-    simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)
-  convert← this
-  rw [← mul_neg_geom_sum, Finset.mul_sum]
+theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * (1 - x) = 1 :=
+  (summable_geometric_of_norm_lt_one h).tsum_pow_mul_one_sub
+
+theorem mul_neg_geom_series (x : R) (h : ‖x‖ < 1) : (1 - x) * ∑' i : ℕ, x ^ i = 1 :=
+  (summable_geometric_of_norm_lt_one h).one_sub_mul_tsum_pow
 
 theorem geom_series_succ (x : R) (h : ‖x‖ < 1) : ∑' i : ℕ, x ^ (i + 1) = ∑' i : ℕ, x ^ i - 1 := by
   rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,

Mathlib/RingTheory/MvPowerSeries/Order.lean

@@ -291,6 +291,13 @@ theorem le_weightedOrder_mul :
       apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
       rw [← hij, map_add, Nat.cast_add]
 
+theorem le_weightedOrder_pow (n : ℕ) : n • f.weightedOrder w ≤ (f ^ n).weightedOrder w := by
+  induction n with
+  | zero => simp
+  | succ n hn =>
+    simpa [add_smul] using
+      le_trans (add_le_add_right hn (f.weightedOrder w)) (le_weightedOrder_mul w)
+
 theorem le_weightedOrder_prod {R : Type*} [CommSemiring R] {ι : Type*} (w : σ → ℕ)
     (f : ι → MvPowerSeries σ R) (s : Finset ι) :
     ∑ i ∈ s, (f i).weightedOrder w ≤ (∏ i ∈ s, f i).weightedOrder w := by
@@ -440,10 +447,24 @@ theorem le_order_mul : f.order + g.order ≤ order (f * g) :=
 
 alias order_mul_ge := le_order_mul
 
+theorem le_order_pow (n : ℕ) : n • f.order ≤ (f ^ n).order :=
+  le_weightedOrder_pow _ n
+
 theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*}
     (f : ι → MvPowerSeries σ R) (s : Finset ι) : ∑ i ∈ s, (f i).order ≤ (∏ i ∈ s, f i).order :=
   le_weightedOrder_prod _ _ _
 
+theorem order_ne_zero_iff_constCoeff_eq_zero :
+    f.order ≠ 0 ↔ f.constantCoeff = 0 := by
+  constructor
+  · intro h
+    apply coeff_of_lt_order
+    simpa using pos_of_ne_zero h
+  · intro h
+    refine ENat.one_le_iff_ne_zero.mp <| MvPowerSeries.le_order fun d hd ↦ ?_
+    rw [Nat.cast_lt_one] at hd
+    simp [(degree_eq_zero_iff d).mp hd, h]
+
 section Ring
 
 variable {R : Type*} [Ring R] {f g : MvPowerSeries σ R}

Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

@@ -290,6 +290,31 @@ theorem summable_of_tendsto_order_atTop_nhds_top
     (h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)) : Summable f :=
   summable_of_tendsto_weightedOrder_atTop_nhds_top h
 
+/-- The geometric series converges if the constant term is zero. -/
+theorem summable_pow_of_constantCoeff_eq_zero {f : MvPowerSeries σ R}
+    (h : f.constantCoeff = 0) : Summable (f ^ ·) := by
+  apply summable_of_tendsto_order_atTop_nhds_top
+  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop]
+  refine fun n ↦ ⟨n + 1, fun m hm ↦ lt_of_lt_of_le ?_ (le_order_pow _)⟩
+  refine (ENat.coe_lt_coe.mpr (Nat.add_one_le_iff.mp hm.le)).trans_le ?_
+  simpa [nsmul_eq_mul] using ENat.self_le_mul_right m (order_ne_zero_iff_constCoeff_eq_zero.mpr h)
+
+section GeomSeries
+variable {R : Type*} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] [T2Space R]
+variable {f : MvPowerSeries σ R}
+
+/-- Formula for geometric series. -/
+theorem tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (h : f.constantCoeff = 0) :
+    (∑' (i : ℕ), f ^ i) * (1 - f) = 1 :=
+  (summable_pow_of_constantCoeff_eq_zero h).tsum_pow_mul_one_sub
+
+/-- Formula for geometric series. -/
+theorem one_sub_mul_tsum_pow_of_constantCoeff_eq_zero (h : f.constantCoeff = 0) :
+    (1 - f) * ∑' (i : ℕ), f ^ i = 1 :=
+  (summable_pow_of_constantCoeff_eq_zero h).one_sub_mul_tsum_pow
+
+end GeomSeries
+
 end Sum
 
 section Prod

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -194,6 +194,18 @@ theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*} (φ : ι → R
 
 alias order_mul_ge := le_order_mul
 
+theorem order_ne_zero_iff_constCoeff_eq_zero {φ : R⟦X⟧} :
+    φ.order ≠ 0 ↔ φ.constantCoeff = 0 := by
+  constructor
+  · intro h
+    rw [← PowerSeries.coeff_zero_eq_constantCoeff]
+    apply coeff_of_lt_order
+    simpa using pos_of_ne_zero h
+  · intro h
+    refine ENat.one_le_iff_ne_zero.mp <| PowerSeries.le_order _ _ fun d hd ↦ ?_
+    rw [Nat.cast_lt_one] at hd
+    simp [hd, h]
+
 /-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise. -/
 theorem order_monomial (n : ℕ) (a : R) [Decidable (a = 0)] :
     order (monomial n a) = if a = 0 then (⊤ : ℕ∞) else n := by

Mathlib/RingTheory/PowerSeries/PiTopology.lean

@@ -156,6 +156,28 @@ theorem summable_of_tendsto_order_atTop_nhds_top [LinearOrder ι] [LocallyFinite
   contrapose! hk
   exact coeff_of_lt_order _ <| by simpa using (hi k hk.le)
 
+variable {R} in
+/-- The geometric series converges if the constant term is zero. -/
+theorem summable_pow_of_constantCoeff_eq_zero {f : PowerSeries R} (h : f.constantCoeff = 0) :
+    Summable (f ^ ·) :=
+  MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero h
+
+section GeomSeries
+variable {R : Type*} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] [T2Space R]
+variable {f : PowerSeries R}
+
+/-- Formula for geometric series. -/
+theorem tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (h : f.constantCoeff = 0) :
+    (∑' (i : ℕ), f ^ i) * (1 - f) = 1 :=
+  (summable_pow_of_constantCoeff_eq_zero h).tsum_pow_mul_one_sub
+
+/-- Formula for geometric series. -/
+theorem one_sub_mul_tsum_pow_of_constantCoeff_eq_zero (h : f.constantCoeff = 0) :
+    (1 - f) * ∑' (i : ℕ), f ^ i = 1 :=
+  (summable_pow_of_constantCoeff_eq_zero h).one_sub_mul_tsum_pow
+
+end GeomSeries
+
 end Sum
 
 section Prod

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

@@ -5,7 +5,9 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
 import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Ring.GeomSum
 import Mathlib.Topology.Algebra.InfiniteSum.Constructions
+import Mathlib.Topology.Algebra.InfiniteSum.NatInt
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Ring.Basic
 
@@ -17,6 +19,7 @@ This file provides lemmas about the interaction between infinite sums and multip
 ## Main results
 
 * `tsum_mul_tsum_eq_tsum_sum_antidiagonal`: Cauchy product formula
+* `Summable.tsum_pow_mul_one_sub`, `Summable.one_sub_mul_tsum_pow`: geometric series formula.
 * `tprod_one_add`: expanding `∏' i : ι, (1 + f i)` as infinite sum.
 -/
 
@@ -249,6 +252,29 @@ end Nat
 
 end CauchyProduct
 
+section GeomSeries
+
+/-!
+### Geometric series `∑' n : ℕ, x ^ n`
+
+This section gives a general result about geometric series without assuming additional structure on
+the topological ring. For normed ring, see also `geom_series_mul_neg` and friends.
+-/
+
+variable [Ring α] [TopologicalSpace α] [IsTopologicalRing α] [T2Space α]
+
+theorem Summable.tsum_pow_mul_one_sub {x : α} (h : Summable (x ^ ·)) :
+    (∑' (i : ℕ), x ^ i) * (1 - x) = 1 := by
+  refine tendsto_nhds_unique (h.hasSum.mul_right (1 - x)).tendsto_sum_nat ?_
+  simpa [← Finset.sum_mul, geom_sum_mul_neg] using tendsto_const_nhds.sub h.tendsto_atTop_zero
+
+theorem Summable.one_sub_mul_tsum_pow {x : α} (h : Summable (x ^ ·)) :
+    (1 - x) * ∑' (i : ℕ), x ^ i = 1 := by
+  refine tendsto_nhds_unique (h.hasSum.mul_left (1 - x)).tendsto_sum_nat ?_
+  simpa [← Finset.mul_sum, mul_neg_geom_sum] using tendsto_const_nhds.sub h.tendsto_atTop_zero
+
+end GeomSeries
+
 section ProdOneSum
 
 /-!