From e6b6302bd4784e1fc139c4f03b06efd186218e78 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Thu, 30 Jan 2025 06:00:14 +0000
Subject: [PATCH] feat(RingTheory/HahnSeries): define powerSeriesFamily
 (#20205)

This PR defines a summable family of power series whose elements are non-negative powers of a fixed Hahn series times the coefficients of a formal power series. We will use it to define algebra homomorphisms from rings of formal power series to Hahn series.
---
 Mathlib.lean                                |   1 +
 Mathlib/RingTheory/HahnSeries/Addition.lean |  20 +++-
 Mathlib/RingTheory/HahnSeries/HEval.lean    | 114 ++++++++++++++++++++
 3 files changed, 132 insertions(+), 3 deletions(-)
 create mode 100644 Mathlib/RingTheory/HahnSeries/HEval.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index f62f59976932f..a16a9e698db7c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4543,6 +4543,7 @@ import Mathlib.RingTheory.GradedAlgebra.Noetherian
 import Mathlib.RingTheory.GradedAlgebra.Radical
 import Mathlib.RingTheory.HahnSeries.Addition
 import Mathlib.RingTheory.HahnSeries.Basic
+import Mathlib.RingTheory.HahnSeries.HEval
 import Mathlib.RingTheory.HahnSeries.Multiplication
 import Mathlib.RingTheory.HahnSeries.PowerSeries
 import Mathlib.RingTheory.HahnSeries.Summable
diff --git a/Mathlib/RingTheory/HahnSeries/Addition.lean b/Mathlib/RingTheory/HahnSeries/Addition.lean
index 01acbffb87646..540db756a8086 100644
--- a/Mathlib/RingTheory/HahnSeries/Addition.lean
+++ b/Mathlib/RingTheory/HahnSeries/Addition.lean
@@ -3,9 +3,10 @@ Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import Mathlib.RingTheory.HahnSeries.Basic
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Module.LinearMap.Defs
+import Mathlib.RingTheory.HahnSeries.Basic
 
 /-!
 # Additive properties of Hahn series
@@ -26,7 +27,7 @@ open Finset Function
 
 noncomputable section
 
-variable {Γ Γ' R S U V : Type*}
+variable {Γ Γ' R S U V α : Type*}
 
 namespace HahnSeries
 
@@ -233,12 +234,25 @@ end Domain
 
 end AddMonoid
 
-instance [AddCommMonoid R] : AddCommMonoid (HahnSeries Γ R) :=
+section AddCommMonoid
+
+variable [AddCommMonoid R]
+
+instance : AddCommMonoid (HahnSeries Γ R) :=
   { inferInstanceAs (AddMonoid (HahnSeries Γ R)) with
     add_comm := fun x y => by
       ext
       apply add_comm }
 
+open BigOperators
+
+@[simp]
+theorem coeff_sum {s : Finset α} {x : α → HahnSeries Γ R} (g : Γ) :
+    (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g :=
+  cons_induction rfl (fun i s his hsum => by rw [sum_cons, sum_cons, add_coeff, hsum]) s
+
+end AddCommMonoid
+
 section AddGroup
 
 variable [AddGroup R]
diff --git a/Mathlib/RingTheory/HahnSeries/HEval.lean b/Mathlib/RingTheory/HahnSeries/HEval.lean
new file mode 100644
index 0000000000000..8af129c21ad4c
--- /dev/null
+++ b/Mathlib/RingTheory/HahnSeries/HEval.lean
@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2024 Scott Carnahan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Carnahan
+-/
+import Mathlib.RingTheory.HahnSeries.Summable
+import Mathlib.RingTheory.PowerSeries.Basic
+
+/-!
+# A summable family given by a power series
+
+## Main Definitions
+ * `HahnSeries.SummableFamily.powerSeriesFamily`: A summable family of Hahn series whose elements
+   are non-negative powers of a fixed positive-order Hahn series multiplied by the coefficients of a
+   formal power series.
+
+## TODO
+ * `PowerSeries.heval`: An `R`-algebra homomorphism from `PowerSeries R` to `HahnSeries Γ R` taking
+   `X` to a positive order Hahn Series.
+
+-/
+
+open Finset Function
+
+open Pointwise
+
+noncomputable section
+
+variable {Γ Γ' R V α β σ : Type*}
+
+namespace HahnSeries
+
+namespace SummableFamily
+
+section PowerSeriesFamily
+
+variable [LinearOrderedCancelAddCommMonoid Γ] [CommRing R]
+
+variable [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (f : PowerSeries R)
+
+/-- A summable family given by scalar multiples of powers of a positive order Hahn series.
+
+The scalar multiples are given by the coefficients of a power series. -/
+abbrev powerSeriesFamily : SummableFamily Γ V ℕ :=
+  smulFamily (fun n => f.coeff R n) (powers x hx)
+
+@[simp]
+theorem powerSeriesFamily_apply (n : ℕ) :
+    powerSeriesFamily hx f n = f.coeff R n • x ^ n :=
+  rfl
+
+theorem powerSeriesFamily_add (g : PowerSeries R) :
+    powerSeriesFamily hx (f + g) = powerSeriesFamily hx f + powerSeriesFamily hx g := by
+  ext1 n
+  simp [add_smul]
+
+theorem powerSeriesFamily_smul (r : R) :
+    powerSeriesFamily hx (r • f) = HahnSeries.single (0 : Γ) r • powerSeriesFamily hx f := by
+  ext1 n
+  simp [mul_smul]
+
+theorem support_powerSeriesFamily_subset (hx : 0 < x.orderTop) (a b : PowerSeries R) (g : Γ) :
+    ((powerSeriesFamily hx (a * b)).coeff g).support ⊆
+    (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support.image
+      fun i => i.1 + i.2 := by
+  simp only [coeff_support, smulFamily_toFun, HahnSeries.smul_coeff, Set.Finite.toFinset_subset,
+    coe_image, support_subset_iff, Set.mem_image, Prod.exists]
+  intro n hn
+  simp_rw [PowerSeries.coeff_mul, sum_smul, mul_smul] at hn
+  have he := exists_ne_zero_of_sum_ne_zero hn
+  simp only [powers_toFun, mem_antidiagonal] at he
+  use he.choose.1, he.choose.2
+  refine ⟨?_, he.choose_spec.1⟩
+  simp only [mul_toFun, smulFamily_toFun, powers_toFun, Algebra.mul_smul_comm,
+    Algebra.smul_mul_assoc, HahnSeries.smul_coeff, Set.Finite.coe_toFinset, ne_eq, Prod.mk.eta,
+    Function.mem_support]
+  rw [← pow_add, smul_comm, he.choose_spec.1]
+  exact he.choose_spec.2
+
+theorem hsum_powerSeriesFamily_mul (hx : 0 < x.orderTop) (a b : PowerSeries R) :
+    (powerSeriesFamily hx (a * b)).hsum =
+    ((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).hsum := by
+  ext g
+  simp only [powerSeriesFamily_apply, PowerSeries.coeff_mul, Finset.sum_smul, ← Finset.sum_product,
+    hsum_coeff_eq_sum, mul_toFun]
+  rw [sum_subset (support_powerSeriesFamily_subset hx a b g)]
+  · rw [← coeff_sum, sum_sigma', coeff_sum]
+    refine (Finset.sum_of_injOn (fun x => ⟨x.1 + x.2, x⟩) (fun _ _ _ _ => by simp_all) ?_ ?_
+      (fun _ _ => by simp only [smul_mul_smul_comm, pow_add])).symm
+    · intro ij hij
+      simp only [coe_sigma, coe_image, Set.mem_sigma_iff, Set.mem_image, Prod.exists, mem_coe,
+        mem_antidiagonal, and_true]
+      use ij.1, ij.2
+      simp_all
+    · intro i hi his
+      have hisc : ∀ j k : ℕ, ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff R k) b •
+          (PowerSeries.coeff R j a • (x ^ j * x ^ k).coeff g) = 0 := by
+        intro m n
+        contrapose!
+        simp only [coeff_support, mul_toFun, smulFamily_toFun, Algebra.mul_smul_comm,
+          Algebra.smul_mul_assoc, Set.Finite.coe_toFinset, Set.mem_image,
+          Prod.exists, not_exists, not_and] at his
+        exact his m n
+      simp only [mem_sigma, mem_antidiagonal] at hi
+      rw [mul_comm ((PowerSeries.coeff R i.snd.1) a), ← hi.2, mul_smul, pow_add]
+      exact hisc i.snd.1 i.snd.2 <| Sigma.eq hi.2 (by simp)
+  · intro i hi his
+    simpa [PowerSeries.coeff_mul, sum_smul] using his
+
+end PowerSeriesFamily
+
+end SummableFamily
+
+end HahnSeries