Documentation

Mathlib.RingTheory.HahnSeries.Summable

Hahn Series #

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on HahnSeries Γ R. We introduce valuations and a notion of summability for possibly infinite families of series.

Main Definitions #

References #

The additive valuation on HahnSeries Γ R, returning the smallest index at which a Hahn Series has a nonzero coefficient, or for the 0 series.

Equations
Instances For
    theorem HahnSeries.addVal_apply {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} :
    (HahnSeries.addVal Γ R) x = if x = 0 then else (HahnSeries.order x)
    @[simp]
    theorem HahnSeries.addVal_apply_of_ne {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (hx : x 0) :
    theorem HahnSeries.addVal_le_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g 0) :
    (HahnSeries.addVal Γ R) x g
    structure HahnSeries.SummableFamily (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [AddCommMonoid R] (α : Type u_3) :
    Type (max (max u_1 u_2) u_3)

    An infinite family of Hahn series which has a formal coefficient-wise sum. The requirements for this are that the union of the supports of the series is well-founded, and that only finitely many series are nonzero at any given coefficient.

    Instances For
      Equations
      • HahnSeries.SummableFamily.instFunLikeSummableFamilyHahnSeriesToZeroToAddMonoid = { coe := HahnSeries.SummableFamily.toFun, coe_injective' := }
      theorem HahnSeries.SummableFamily.isPWO_iUnion_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) :
      Set.IsPWO (⋃ (a : α), HahnSeries.support (s a))
      theorem HahnSeries.SummableFamily.finite_co_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) (g : Γ) :
      Set.Finite (Function.support fun (a : α) => (s a).coeff g)
      theorem HahnSeries.SummableFamily.coe_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} :
      Function.Injective DFunLike.coe
      theorem HahnSeries.SummableFamily.ext {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} (h : ∀ (a : α), s a = t a) :
      s = t
      Equations
      • HahnSeries.SummableFamily.instAddSummableFamily = { add := fun (x y : HahnSeries.SummableFamily Γ R α) => { toFun := x + y, isPWO_iUnion_support' := , finite_co_support' := } }
      Equations
      • HahnSeries.SummableFamily.instZeroSummableFamily = { zero := { toFun := 0, isPWO_iUnion_support' := , finite_co_support' := } }
      Equations
      • HahnSeries.SummableFamily.instInhabitedSummableFamily = { default := 0 }
      @[simp]
      theorem HahnSeries.SummableFamily.coe_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} :
      (s + t) = s + t
      theorem HahnSeries.SummableFamily.add_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} {a : α} :
      (s + t) a = s a + t a
      @[simp]
      theorem HahnSeries.SummableFamily.coe_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} :
      0 = 0
      theorem HahnSeries.SummableFamily.zero_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {a : α} :
      0 a = 0
      Equations
      def HahnSeries.SummableFamily.hsum {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) :

      The infinite sum of a SummableFamily of Hahn series.

      Equations
      Instances For
        @[simp]
        theorem HahnSeries.SummableFamily.hsum_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {g : Γ} :
        (HahnSeries.SummableFamily.hsum s).coeff g = finsum fun (i : α) => (s i).coeff g
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        @[simp]
        theorem HahnSeries.SummableFamily.coe_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} :
        (-s) = -s
        theorem HahnSeries.SummableFamily.neg_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {a : α} :
        (-s) a = -s a
        @[simp]
        theorem HahnSeries.SummableFamily.coe_sub {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} :
        (s - t) = s - t
        theorem HahnSeries.SummableFamily.sub_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} {a : α} :
        (s - t) a = s a - t a
        @[simp]
        theorem HahnSeries.SummableFamily.smul_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ R α} {a : α} :
        (x s) a = x * s a
        @[simp]
        theorem HahnSeries.SummableFamily.lsum_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) :
        HahnSeries.SummableFamily.lsum s = HahnSeries.SummableFamily.hsum s

        The summation of a summable_family as a LinearMap.

        Equations
        • HahnSeries.SummableFamily.lsum = { toAddHom := { toFun := HahnSeries.SummableFamily.hsum, map_add' := }, map_smul' := }
        Instances For
          def HahnSeries.SummableFamily.ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (f : α →₀ HahnSeries Γ R) :

          A family with only finitely many nonzero elements is summable.

          Equations
          Instances For
            @[simp]
            def HahnSeries.SummableFamily.embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α β) :

            A summable family can be reindexed by an embedding without changing its sum.

            Equations
            Instances For
              theorem HahnSeries.SummableFamily.embDomain_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α β) {b : β} :
              (HahnSeries.SummableFamily.embDomain s f) b = if h : b Set.range f then s (Classical.choose h) else 0
              @[simp]
              theorem HahnSeries.SummableFamily.embDomain_image {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α β) {a : α} :
              @[simp]
              theorem HahnSeries.SummableFamily.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α β) {b : β} (h : bSet.range f) :

              The powers of an element of positive valuation form a summable family.

              Equations
              Instances For
                theorem HahnSeries.unit_aux {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R] (x : HahnSeries Γ R) {r : R} (hr : r * x.coeff (HahnSeries.order x) = 1) :
                0 < (HahnSeries.addVal Γ R) (1 - HahnSeries.C r * (HahnSeries.single (-HahnSeries.order x)) 1 * x)
                theorem HahnSeries.isUnit_iff {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} :
                Equations
                • One or more equations did not get rendered due to their size.