feat(RingTheory/HahnSeries/Basic): Make a Hahn series from a function…

… with support bounded below (#9574)

Given a locally finite linearly ordered set `Γ` and a function `f` on `Γ` whose support is bounded below, we produce a Hahn series whose coefficients are given by `f`.  We introduce a theorem (borrowing from mathlib3 #18604) for translating the vanishing condition to the partially well-ordered support condition that is used in the definition of Hahn Series.

Mathlib/Order/WellFoundedSet.lean

@@ -702,6 +702,22 @@ end Set
 
 open Set
 
+section LocallyFiniteOrder
+
+variable {s : Set α} [Preorder α] [LocallyFiniteOrder α]
+
+theorem BddBelow.wellFoundedOn_lt : BddBelow s → s.WellFoundedOn (· < ·) := by
+  rw [wellFoundedOn_iff_no_descending_seq]
+  rintro ⟨a, ha⟩ f hf
+  refine infinite_range_of_injective f.injective ?_
+  exact (finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
+    ⟨ha <| hf _, antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| zero_le _⟩
+
+theorem BddAbove.wellFoundedOn_gt : BddAbove s → s.WellFoundedOn (· > ·) :=
+  fun h => h.dual.wellFoundedOn_lt
+
+end LocallyFiniteOrder
+
 namespace Set.PartiallyWellOrderedOn
 
 variable {r : α → α → Prop}

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -350,4 +350,47 @@ end Domain
 
 end Zero
 
+section LocallyFiniteLinearOrder
+
+variable [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ]
+
+theorem suppBddBelow_supp_PWO (f : Γ → R) (hf : BddBelow (Function.support f)) :
+    (Function.support f).IsPWO := Set.isWF_iff_isPWO.mp hf.wellFoundedOn_lt
+
+theorem forallLTEqZero_supp_BddBelow (f : Γ → R) (n : Γ) (hn : ∀(m : Γ), m < n → f m = 0) :
+    BddBelow (Function.support f) := by
+  unfold BddBelow Set.Nonempty lowerBounds
+  use n
+  intro m hm
+  rw [Function.mem_support, ne_eq] at hm
+  exact not_lt.mp (mt (hn m) hm)
+
+/-- Construct a Hahn series from any function whose support is bounded below. -/
+@[simps]
+def ofSuppBddBelow (f : Γ → R) (hf : BddBelow (Function.support f)) : HahnSeries Γ R where
+  coeff := f
+  isPWO_support' := suppBddBelow_supp_PWO f hf
+
+theorem BddBelow_zero [Nonempty Γ] : BddBelow (Function.support (0 : Γ → R)) := by
+  simp only [support_zero', bddBelow_empty]
+
+@[simp]
+theorem zero_ofSuppBddBelow [Nonempty Γ] : ofSuppBddBelow 0 BddBelow_zero = (0 : HahnSeries Γ R) :=
+  rfl
+
+theorem order_ofForallLtEqZero [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ)
+    (hn : ∀(m : Γ), m < n → f m = 0) :
+    n ≤ order (ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)) := by
+  dsimp only [order]
+  by_cases h : ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn) = 0
+  cases h
+  exact (hf rfl).elim
+  simp_all only [dite_false]
+  rw [Set.IsWF.le_min_iff]
+  intro m hm
+  rw [HahnSeries.support, Function.mem_support, ne_eq] at hm
+  exact not_lt.mp (mt (hn m) hm)
+
+end LocallyFiniteLinearOrder
+
 end HahnSeries

Mathlib/RingTheory/LaurentSeries.lean

@@ -22,7 +22,6 @@ import Mathlib.RingTheory.Localization.FractionRing
 
 -/
 
-
 open scoped Classical
 open HahnSeries BigOperators Polynomial
 
@@ -35,7 +34,7 @@ abbrev LaurentSeries (R : Type*) [Zero R] :=
   HahnSeries ℤ R
 #align laurent_series LaurentSeries
 
-variable {R : Type u}
+variable {R : Type*}
 
 namespace LaurentSeries