feat (RingTheory/HahnSeries): introduce binomialFamily and generalized powers. (#31215)

We introduce a way to take generalized powers of Hahn series whose leading term is 1. The powers take values in a binomial ring.

Author: ScottCarnahan

Mathlib.lean

@@ -5811,6 +5811,7 @@ public import Mathlib.RingTheory.GradedAlgebra.Radical
 public import Mathlib.RingTheory.Grassmannian
 public import Mathlib.RingTheory.HahnSeries.Addition
 public import Mathlib.RingTheory.HahnSeries.Basic
+public import Mathlib.RingTheory.HahnSeries.Binomial
 public import Mathlib.RingTheory.HahnSeries.HEval
 public import Mathlib.RingTheory.HahnSeries.HahnEmbedding
 public import Mathlib.RingTheory.HahnSeries.Lex

Mathlib/RingTheory/HahnSeries/Addition.lean

@@ -72,6 +72,10 @@ theorem orderTop_smul_not_lt (r : R) (x : HahnSeries Γ V) : ¬ (r • x).orderT
     exact Set.IsWF.min_of_subset_not_lt_min
       (Function.support_smul_subset_right (fun _ => r) x.coeff)
 
+theorem orderTop_le_orderTop_smul {Γ} [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) :
+    x.orderTop ≤ (r • x).orderTop :=
+  le_of_not_gt <| orderTop_smul_not_lt r x
+
 theorem order_smul_not_lt [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
     ¬ (r • x).order < x.order := by
   have hx : x ≠ 0 := right_ne_zero_of_smul h
@@ -418,6 +422,24 @@ theorem leadingCoeff_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R}
   rw [← orderTop_neg (x := y)] at hxy
   exact leadingCoeff_add_eq_left hxy
 
+theorem orderTop_sub_ne {x y : HahnSeries Γ R} {g : Γ}
+    (hxg : x.orderTop = g) (hyg : y.orderTop = g) (hxyc : x.leadingCoeff = y.leadingCoeff) :
+    (x - y).orderTop ≠ g := by
+  refine orderTop_ne_of_coeff_eq_zero ?_
+  have hx : x ≠ 0 := fun h ↦ by simp_all [orderTop_zero, WithTop.top_ne_coe]
+  rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hxg
+  have hy : y ≠ 0 := fun h ↦ by simp_all [orderTop_zero, WithTop.top_ne_coe]
+  rw [orderTop_of_ne_zero hy, WithTop.coe_eq_coe] at hyg
+  simp only [leadingCoeff_of_ne_zero hx, leadingCoeff_of_ne_zero hy, untop_orderTop_of_ne_zero hx,
+    untop_orderTop_of_ne_zero hy, hxg, hyg] at hxyc
+  rwa [coeff_sub, sub_eq_zero]
+
+theorem le_orderTop_of_leadingCoeff_eq {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} {g : Γ}
+    (hxg : x.orderTop = g) (hyg : y.orderTop = g) (hxyc : x.leadingCoeff = y.leadingCoeff) :
+    g < (x - y).orderTop :=
+  lt_of_le_of_ne (le_of_eq_of_le (by rw [hxg, hyg, inf_idem]) min_orderTop_le_orderTop_sub)
+    (orderTop_sub_ne hxg hyg hxyc).symm
+
 end AddGroup
 
 instance [AddCommGroup R] : AddCommGroup (HahnSeries Γ R) :=

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -280,6 +280,10 @@ theorem coeff_orderTop_ne {x : HahnSeries Γ R} {g : Γ} (hg : x.orderTop = g) :
   rw [← hg]
   exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)
 
+theorem orderTop_ne_of_coeff_eq_zero {x : HahnSeries Γ R} {i : Γ} (hx : x.coeff i = 0) :
+    x.orderTop ≠ i :=
+  fun h ↦ coeff_orderTop_ne h hx
+
 theorem orderTop_le_of_coeff_ne_zero {Γ} [LinearOrder Γ] {x : HahnSeries Γ R}
     {g : Γ} (h : x.coeff g ≠ 0) : x.orderTop ≤ g := by
   rw [orderTop_of_ne_zero (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]

Mathlib/RingTheory/HahnSeries/Binomial.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2024 Scott Carnahan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Carnahan
+-/
+module
+
+public import Mathlib.RingTheory.HahnSeries.HEval
+public import Mathlib.RingTheory.PowerSeries.Binomial
+
+/-!
+# Binomial expansions of powers of Hahn Series
+We introduce binomial expansions using `embDomain`.
+
+## Main Definitions
+  * `HahnSeries.binomialFamily`
+
+## Main results
+  * coefficients of powers of binomials
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace HahnSeries
+
+variable {Γ R A : Type*}
+
+variable [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R]
+  [BinomialRing R]
+
+namespace SummableFamily
+
+variable [CommRing A] [Algebra R A]
+
+/-- A summable family of Hahn series, whose `n`th term is `Ring.choose r n • (x - 1) ^ n` when
+`x` is close to `1` (more precisely, when `0 < (x - 1).orderTop`), and `0 ^ n` otherwise. These
+terms give a formal expansion of `x ^ r` as `(1 + (x - 1)) ^ r`. -/
+def binomialFamily (x : HahnSeries Γ A) (r : R) :
+    SummableFamily Γ A ℕ :=
+  powerSeriesFamily (x - 1) (PowerSeries.binomialSeries A r)
+
+@[simp]
+theorem binomialFamily_apply {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop) (r : R) (n : ℕ) :
+    binomialFamily x r n = Ring.choose r n • (x - 1) ^ n := by
+  simp [hx, binomialFamily]
+
+@[simp]
+theorem binomialFamily_apply_of_orderTop_nonpos {x : HahnSeries Γ A} (hx : ¬ 0 < (x - 1).orderTop)
+    (r : R) (n : ℕ) :
+    binomialFamily x r n = 0 ^ n := by
+  rw [binomialFamily, powerSeriesFamily_of_not_orderTop_pos hx]
+  by_cases hn : n = 0 <;> simp [hn]
+
+theorem binomialFamily_orderTop_pos {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop) (r : R) {n : ℕ}
+    (hn : 0 < n) :
+    0 < (binomialFamily x r n).orderTop := by
+  simp only [binomialFamily, smulFamily_toFun, PowerSeries.binomialSeries_coeff, powers_toFun, hx,
+    ↓reduceIte, smul_assoc, one_smul]
+  have : n ≠ 0 := by exact Nat.ne_zero_of_lt hn
+  calc
+    0 < n • (x - 1).orderTop := (nsmul_pos_iff (Nat.ne_zero_of_lt hn)).mpr hx
+    n • (x - 1).orderTop ≤ ((x - 1) ^ n).orderTop := orderTop_nsmul_le_orderTop_pow
+    ((x - 1) ^ n).orderTop ≤ ((Ring.choose r n) • ((x - 1) ^ n)).orderTop :=
+      orderTop_le_orderTop_smul (Ring.choose r n) ((x - 1) ^ n)
+
+theorem binomialFamily_mem_support {x : HahnSeries Γ A}
+    (hx : 0 < (x - 1).orderTop) (r : R) (n : ℕ) {g : Γ}
+    (hg : g ∈ (binomialFamily x r n).support) : 0 ≤ g := by
+  by_cases hn : n = 0; · simp_all
+  exact le_of_lt (WithTop.coe_pos.mp (lt_of_lt_of_le (binomialFamily_orderTop_pos hx r
+    (Nat.pos_of_ne_zero hn)) (orderTop_le_of_coeff_ne_zero hg)))
+
+theorem orderTop_hsum_binomialFamily_pos {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop)
+    (r : R) : (0 : WithTop Γ) < (SummableFamily.hsum (binomialFamily x r) - 1).orderTop := by
+  obtain (_|_) := subsingleton_or_nontrivial A
+  · simp [Subsingleton.eq_zero ((binomialFamily x r).hsum - 1)]
+  · refine (orderTop_self_sub_one_pos_iff (binomialFamily x r).hsum).mpr ?_
+    constructor
+    · exact hsum_orderTop_of_le (by simp [hx]) (fun b g hg => binomialFamily_mem_support
+        hx r b hg) fun b hb => coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
+        Nat.zero_lt_of_ne_zero hb
+    · have : (binomialFamily x r 0).coeff 0 = 1 := by simp [hx]
+      rw [← this]
+      refine hsum_leadingCoeff_of_le (g := 0) (a := 0) (by simp [hx]) ?_ ?_
+      · intro b g' hg'
+        exact binomialFamily_mem_support hx r b hg'
+      · intro b hb
+        exact coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
+        Nat.zero_lt_of_ne_zero hb
+
+end SummableFamily
+
+open SummableFamily
+
+instance : Pow (orderTopSubOnePos Γ R) R where
+  pow x r := toOrderTopSubOnePos (orderTop_hsum_binomialFamily_pos x.2 r)
+
+@[simp]
+theorem binomial_power {x : orderTopSubOnePos Γ R} {r : R} :
+    x ^ r = toOrderTopSubOnePos (orderTop_hsum_binomialFamily_pos x.2 r) :=
+  rfl
+
+theorem pow_add {x : orderTopSubOnePos Γ R} {r s : R} : x ^ (r + s) = x ^ r * x ^ s := by
+  suffices (x ^ (r + s)).val = (x ^ r * x ^ s).val by exact SetLike.coe_eq_coe.mp this
+  suffices (x ^ (r + s)).val.val = (x ^ r * x ^ s).val.val by exact Units.val_inj.mp this
+  simp [binomialFamily, hsum_powerSeriesFamily_mul, hsum_mul]
+
+theorem coeff_toOrderTopSubOnePos_pow {g : Γ} (hg : 0 < g) (r s : R) (k : ℕ) :
+    HahnSeries.coeff (toOrderTopSubOnePos (orderTop_sub_pos hg r) ^ s).val (k • g) =
+      Ring.choose s k • r ^ k := by
+  simp only [val_toOrderTopSubOnePos_coe, binomial_power, coeff_hsum, smul_eq_mul]
+  rw [finsum_eq_single _ k, binomialFamily_apply (orderTop_sub_pos hg r), add_sub_cancel_left,
+    single_pow, coeff_smul, coeff_single_same (k • g) (r ^ k), smul_eq_mul]
+  intro n hn
+  rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
+    smul_zero]
+  · contrapose! hn
+    apply (StrictMono.injective (nsmul_left_strictMono hg)) hn.symm
+  · by_cases hr : r = 0 <;> simp [hr, hg]
+
+end HahnSeries

Mathlib/RingTheory/HahnSeries/Multiplication.lean

@@ -33,6 +33,8 @@ with the action of `HahnSeries Γ R` on `HahnModule Γ' R V`.
 * `HahnSeries.C` is the `constant term` ring homomorphism `R →+* HahnSeries Γ R`.
 * `HahnSeries.embDomainRingHom` is the ring homomorphism `HahnSeries Γ R →+* HahnSeries Γ' R`
   induced by an order embedding `Γ ↪o Γ'`.
+* `HahnSeries.orderTopSubOnePos` is the group of invertible Hahn series close to 1, i.e., those
+  series such that subtracting one yields a series with strictly positive `orderTop`.
 
 ## Main results
 * If `R` is a (commutative) (semi-)ring, then so is `HahnSeries Γ R`.
@@ -85,7 +87,7 @@ theorem support_one [MulZeroOneClass R] [Nontrivial R] : support (1 : HahnSeries
   support_single_of_ne one_ne_zero
 
 @[simp]
-theorem orderTop_one [MulZeroOneClass R] [Nontrivial R] : orderTop (1 : HahnSeries Γ R) = 0 := by
+theorem orderTop_one [Zero R] [One R] [NeZero (1 : R)] : orderTop (1 : HahnSeries Γ R) = 0 := by
   rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]
 
 @[simp]
@@ -391,10 +393,12 @@ end DistribSMul
 
 end HahnModule
 
-variable [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
-
 namespace HahnSeries
 
+section mul
+
+variable [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
+
 instance [NonUnitalNonAssocSemiring R] : Mul (HahnSeries Γ R) where
   mul x y := (HahnModule.of R).symm (x • HahnModule.of R y)
 
@@ -492,16 +496,41 @@ theorem support_mul_subset_add_support [NonUnitalNonAssocSemiring R] {x y : Hahn
   rw [← of_symm_smul_of_eq_mul, ← vadd_eq_add]
   exact HahnModule.support_smul_subset_vadd_support
 
+instance [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R) :=
+  { inferInstanceAs (AddCommMonoid (HahnSeries Γ R)),
+    inferInstanceAs (Distrib (HahnSeries Γ R)) with
+    zero_mul := fun _ => by
+      ext
+      simp [coeff_mul]
+    mul_zero := fun _ => by
+      ext
+      simp [coeff_mul] }
+
+end mul
+
 section orderLemmas
 
-variable {Γ : Type*} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ]
+variable [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ]
   [NonUnitalNonAssocSemiring R]
 
 theorem coeff_mul_order_add_order (x y : HahnSeries Γ R) :
     (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff := by
   simp only [← of_symm_smul_of_eq_mul]
   exact HahnModule.coeff_smul_order_add_order x y
 
+theorem orderTop_mul_of_nonzero {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) :
+    (x * y).orderTop = x.orderTop + y.orderTop := by
+  by_cases hx : x = 0; · simp [hx]
+  by_cases hy : y = 0; · simp [hy]
+  have : (x * y).coeff (x.order + y.order) ≠ 0 := by rwa [coeff_mul_order_add_order x y]
+  have hxy : x * y ≠ 0 := fun h ↦ (by simp [h] at this)
+  rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
+    ← order_eq_orderTop_of_ne_zero hxy, ← WithTop.coe_add, WithTop.coe_eq_coe]
+  refine le_antisymm (order_le_of_coeff_ne_zero this) ?_
+  rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, HahnSeries.order_of_ne hxy,
+    ← Set.IsWF.min_add]
+  exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support
+
 theorem orderTop_add_le_mul {x y : HahnSeries Γ R} :
     x.orderTop + y.orderTop ≤ (x * y).orderTop := by
   rw [← smul_eq_mul]
@@ -519,6 +548,11 @@ theorem order_mul_of_nonzero {x y : HahnSeries Γ R}
     order_of_ne <| ne_zero_of_coeff_ne_zero hxy, ← Set.IsWF.min_add]
   exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support
 
+theorem leadingCoeff_mul_of_nonzero {x y : HahnSeries Γ R}
+    (h : x.leadingCoeff * y.leadingCoeff ≠ 0) :
+    (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff := by
+  simp only [leadingCoeff_eq, order_mul_of_nonzero h, coeff_mul_order_add_order]
+
 theorem order_single_mul_of_isRegular {g : Γ} {r : R} (hr : IsRegular r)
     {x : HahnSeries Γ R} (hx : x ≠ 0) : (((single g) r) * x).order = g + x.order := by
   obtain _ | _ := subsingleton_or_nontrivial R
@@ -529,6 +563,10 @@ theorem order_single_mul_of_isRegular {g : Γ} {r : R} (hr : IsRegular r)
 
 end orderLemmas
 
+section ring
+
+variable [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
+
 private theorem mul_assoc' [NonUnitalSemiring R] (x y z : HahnSeries Γ R) :
     x * y * z = x * (y * z) := by
   ext b
@@ -539,16 +577,6 @@ private theorem mul_assoc' [NonUnitalSemiring R] (x y z : HahnSeries Γ R) :
     (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
     aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])
 
-instance [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R) :=
-  { inferInstanceAs (AddCommMonoid (HahnSeries Γ R)),
-    inferInstanceAs (Distrib (HahnSeries Γ R)) with
-    zero_mul := fun _ => by
-      ext
-      simp [coeff_mul]
-    mul_zero := fun _ => by
-      ext
-      simp [coeff_mul] }
-
 instance [NonUnitalSemiring R] : NonUnitalSemiring (HahnSeries Γ R) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (HahnSeries Γ R)) with
     mul_assoc := mul_assoc' }
@@ -603,15 +631,18 @@ instance [CommRing R] : CommRing (HahnSeries Γ R) :=
   { inferInstanceAs (CommSemiring (HahnSeries Γ R)),
     inferInstanceAs (Ring (HahnSeries Γ R)) with }
 
-theorem orderTop_nsmul_le_orderTop_pow {Γ}
-    [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ]
-    [Semiring R] {x : HahnSeries Γ R} {n : ℕ} : n • x.orderTop ≤ (x ^ n).orderTop := by
+end ring
+
+theorem orderTop_nsmul_le_orderTop_pow [AddCommMonoid Γ] [LinearOrder Γ]
+    [IsOrderedCancelAddMonoid Γ] [Semiring R] {x : HahnSeries Γ R} {n : ℕ} :
+    n • x.orderTop ≤ (x ^ n).orderTop := by
   induction n with
   | zero =>
     simp only [zero_smul, pow_zero]
-    by_cases h : (0 : R) = 1
-    · simp [subsingleton_iff_zero_eq_one.mp h]
-    · simp [nontrivial_of_ne 0 1 h]
+    by_cases h : NeZero (1 : R)
+    · simp
+    · have : Subsingleton R := not_nontrivial_iff_subsingleton.mp fun _ ↦ h NeZero.one
+      simp
   | succ n ih =>
     rw [add_nsmul, pow_add]
     calc
@@ -620,8 +651,64 @@ theorem orderTop_nsmul_le_orderTop_pow {Γ}
       (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
       (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
 
+theorem orderTop_self_sub_one_pos_iff [LinearOrder Γ] [Zero Γ] [NonAssocRing R] [Nontrivial R]
+    (x : HahnSeries Γ R) :
+    0 < (x - 1).orderTop ↔ x.orderTop = 0 ∧ x.leadingCoeff = 1 := by
+  constructor
+  · intro hx
+    constructor
+    · rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]
+      exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)
+    · rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]
+      exact leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)
+  · intro h
+    refine lt_of_le_of_ne (le_of_eq_of_le (by simp_all)
+      (min_orderTop_le_orderTop_sub (Γ := Γ) (R := R))) <| Ne.symm <|
+      orderTop_sub_ne h.1 orderTop_one ?_
+    rw [h.2, leadingCoeff_one]
+
+theorem orderTop_sub_pos [PartialOrder Γ] [Zero Γ] [AddCommGroup R] [One R] {g : Γ} (hg : 0 < g)
+    (r : R) :
+    0 < ((1 + single g r) - 1).orderTop := by
+  by_cases hr : r = 0 <;> simp [hr, hg]
+
+/-- The group of invertible Hahn series close to 1, i.e., those series such that subtracting 1
+  yields a series with strictly positive `orderTop`. -/
+def orderTopSubOnePos (Γ R) [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ]
+    [CommRing R] : Subgroup (HahnSeries Γ R)ˣ where
+  carrier := { x : (HahnSeries Γ R)ˣ | 0 < (x.val - 1).orderTop}
+  mul_mem' := by
+    intro x y hx hy
+    obtain (_|_) := subsingleton_or_nontrivial R
+    · simp
+    · simp_all only [Set.mem_setOf_eq, orderTop_self_sub_one_pos_iff]
+      have h1 : x.val.leadingCoeff * y.val.leadingCoeff = 1 := by rw [hx.2, hy.2, mul_one]
+      constructor
+      · rw [Units.val_mul, orderTop_mul_of_nonzero (by simp [h1]), hx.1, hy.1, add_zero]
+      · rw [Units.val_mul, leadingCoeff_mul_of_nonzero (h1 ▸ one_ne_zero), h1]
+  one_mem' := by simp
+  inv_mem' {y} h := by
+    suffices 0 < (y.inv - 1).orderTop by exact this
+    obtain (_|_) := subsingleton_or_nontrivial R
+    · simp
+    · have : 0 < (y.val - 1).orderTop := h
+      rw [orderTop_self_sub_one_pos_iff] at this
+      have nz : y.val.leadingCoeff * y.inv.leadingCoeff ≠ 0 := by
+        rw [this.2, one_mul]
+        exact leadingCoeff_ne_zero.mpr (by simp)
+      refine y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩
+      · simpa [this.1, y.val_inv] using (orderTop_mul_of_nonzero nz).symm
+      · simpa [this.2, y.val_inv] using (leadingCoeff_mul_of_nonzero nz).symm
+
+@[simp]
+theorem mem_orderTopSubOnePos_iff [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ]
+    [CommRing R] (x : (HahnSeries Γ R)ˣ) :
+    x ∈ orderTopSubOnePos Γ R ↔ 0 < (x.val - 1).orderTop := .rfl
+
 end HahnSeries
 
+variable [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
+
 namespace HahnModule
 
 variable [PartialOrder Γ'] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V]