Novikov series

Let H be an additive group and N : H →+ ℝ a period homomorphism. A Novikov series with coefficients in R is a coefficient function a : H → R with only finitely many nonzero coefficients below every real period cutoff: {h | a h ≠ 0 ∧ N h < C} is finite for every C : ℝ. Under convolution, these series form the Novikov completion of the group ring R[H] along the period filtration; it is the coefficient ring of the Novikov complex of a closed one-form whose periods are recorded by N.

Neither injectivity nor discreteness of N is assumed: finitely many nonzero coefficients may share a period value, and the periods of an infinite support tend to +∞.

This file sets up the carrier and its additive structure, the monomials, and the finiteness facts on which the convolution product of TauCeti.RingTheory.NovikovSeries.Multiplication rests. The design of the additive API follows that of Mathlib's HahnSeries in Mathlib/RingTheory/HahnSeries/Addition.lean; no code is copied from there.

Main definitions

• TauCeti.NovikovSeries R H N: Novikov series over R on H for the period map N.
• TauCeti.NovikovSeries.ofFinsupp: a finitely supported coefficient function as a Novikov series.
• TauCeti.NovikovSeries.single: the monomial r e^h, with coefficient r at h and 0 elsewhere.
• TauCeti.NovikovSeries.order: the least period of the support of a Novikov series, and 0 for the zero series.
• TauCeti.NovikovSeries.trunc C a: the finitely supported truncation of a below the period cutoff C.

Main results

• TauCeti.NovikovSeries.forall_finite_lt_iff_forall_finite_le: the support condition may be stated with N h ≤ C in place of N h < C.
• TauCeti.NovikovSeries.bddBelow_image_support and TauCeti.NovikovSeries.exists_isLeast_image_support: the periods of the support are bounded below, and a nonzero series attains a least period on its support.
• TauCeti.NovikovSeries.finite_support_of_bddAbove_image: a Novikov series whose periods are bounded above on its support has finite support.
• TauCeti.NovikovSeries.isLeast_order: the order of a nonzero series is the least period of its support.
• TauCeti.NovikovSeries.min_order_le_order_add: the order of a nonzero sum is at least the smaller of the orders of the summands.
• TauCeti.NovikovSeries.forall_finite_lt_iff_bddBelow_support: on ℤ with the period map k ↦ k, the support condition says exactly that the support is bounded below.
• TauCeti.NovikovSeries.finite_setOf_period_add_lt: for two Novikov series, the pairs of support exponents whose sum has period below a fixed cutoff form a finite set. In particular (TauCeti.NovikovSeries.finite_setOf_add_eq) each coefficient of the convolution is a finite sum.
• TauCeti.NovikovSeries.finite_setOf_period_add_add_lt and TauCeti.NovikovSeries.finite_setOf_add_add_eq: the same uniform cutoff finiteness for triples of support exponents, on which associativity of the convolution rests.
• TauCeti.NovikovSeries.ofFinsupp_surjective_iff: over a nontrivial coefficient type, every Novikov series is finitely supported if and only if N = 0.

References

• M. Hutchings and Y.-J. Lee, Circle-valued Morse theory and Reidemeister torsion, Geom. Topol. 3 (1999), Section 2.
• A. Pajitnov, Circle-valued Morse Theory, de Gruyter 2006, Chapter 3.

structure TauCeti.NovikovSeries (R : Type u_1) (H : Type u_2) [Zero R] [AddZeroClass H] (N : H →+ ℝ) : Type (max u_1 u_2)

A Novikov series over R on the additive group H, for the period homomorphism N : H →+ ℝ: a coefficient function H → R with only finitely many nonzero coefficients below each real period cutoff.

• coeff : H → R

  The coefficient of a Novikov series at an exponent.

• finite_lt (C : ℝ) : {h : H | self.coeff h ≠ 0 ∧ N h < C}.Finite

  Only finitely many coefficients are nonzero below each period cutoff.

theorem TauCeti.NovikovSeries.coeff_injective {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} : Function.Injective coeff

theorem TauCeti.NovikovSeries.ext {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a b : NovikovSeries R H N} (h : ∀ (g : H), a.coeff g = b.coeff g) : a = b

theorem TauCeti.NovikovSeries.ext_iff {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a b : NovikovSeries R H N} : a = b ↔ ∀ (g : H), a.coeff g = b.coeff g

def TauCeti.NovikovSeries.support {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} (a : NovikovSeries R H N) : Set H

The support of a Novikov series: the exponents with nonzero coefficient.

@[simp]

theorem TauCeti.NovikovSeries.mem_support {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a : NovikovSeries R H N} {h : H} : h ∈ a.support ↔ a.coeff h ≠ 0

theorem TauCeti.NovikovSeries.forall_finite_lt_iff_forall_finite_le {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} (f : H → R) : (∀ (C : ℝ), {h : H | f h ≠ 0 ∧ N h < C}.Finite) ↔ ∀ (C : ℝ), {h : H | f h ≠ 0 ∧ N h ≤ C}.Finite

The support condition of Novikov series is equivalent to the one with non-strict period cutoffs.

theorem TauCeti.NovikovSeries.finite_le {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} (a : NovikovSeries R H N) (C : ℝ) : {h : H | a.coeff h ≠ 0 ∧ N h ≤ C}.Finite

theorem TauCeti.NovikovSeries.finite_support_of_bddAbove_image {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a : NovikovSeries R H N} (h : BddAbove (⇑N '' a.support)) : a.support.Finite

If the periods are bounded above on the support of a Novikov series, for instance if they vanish, the series has finite support: a single period cutoff lies above all of its exponents.

theorem TauCeti.NovikovSeries.bddBelow_image_support {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} (a : NovikovSeries R H N) : BddBelow (⇑N '' a.support)

The periods of the support of a Novikov series are bounded below.

theorem TauCeti.NovikovSeries.exists_isLeast_image_support {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a : NovikovSeries R H N} (ha : a.support.Nonempty) : ∃ h ∈ a.support, IsLeast (⇑N '' a.support) (N h)

A Novikov series with nonempty support attains a least period on its support.

theorem TauCeti.NovikovSeries.forall_finite_lt_iff_bddBelow_support {R : Type u_1} [Zero R] (f : ℤ → R) : (∀ (C : ℝ), {k : ℤ | f k ≠ 0 ∧ (Int.castAddHom ℝ) k < C}.Finite) ↔ BddBelow (Function.support f)

On the exponent group ℤ with the period map k ↦ k, a coefficient function has only finitely many nonzero coefficients below every real cutoff if and only if its support is bounded below.

theorem TauCeti.NovikovSeries.bddBelow_support_int {R : Type u_1} [Zero R] (a : NovikovSeries R ℤ (Int.castAddHom ℝ)) : BddBelow a.support

The support of a Novikov series on ℤ for the period map k ↦ k is bounded below.

@[instance_reducible]

instance TauCeti.NovikovSeries.instZero {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} : Zero (NovikovSeries R H N)

The zero Novikov series.

@[simp]

theorem TauCeti.NovikovSeries.coeff_zero' {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} : coeff 0 = 0

theorem TauCeti.NovikovSeries.coeff_zero {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} (h : H) : coeff 0 h = 0

@[simp]

theorem TauCeti.NovikovSeries.support_zero {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} : support 0 = ∅

@[simp]

theorem TauCeti.NovikovSeries.support_eq_empty {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a : NovikovSeries R H N} : a.support = ∅ ↔ a = 0

theorem TauCeti.NovikovSeries.support_nonempty_iff {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} {a : NovikovSeries R H N} : a.support.Nonempty ↔ a ≠ 0

@[instance_reducible]

instance TauCeti.NovikovSeries.instInhabited {R : Type u_1} {H : Type u_2} [Zero R] [AddZeroClass H] {N : H →+ ℝ} : Inhabited (NovikovSeries R H N)

theorem TauCeti.NovikovSeries.finite_setOf_period_add_lt {R : Type u_1} {S : Type u_2} {H : Type u_3} [Zero R] [Zero S] [AddZeroClass H] {N : H →+ ℝ} (a : NovikovSeries R H N) (b : NovikovSeries S H N) (C : ℝ) : {p : H × H | N (p.1 + p.2) < C ∧ a.coeff p.1 ≠ 0 ∧ b.coeff p.2 ≠ 0}.Finite

Uniform cutoff finiteness for convolution: for Novikov series a and b, only finitely many pairs (u, v) of support exponents have N (u + v) < C.

theorem TauCeti.NovikovSeries.finite_setOf_add_eq {R : Type u_1} {S : Type u_2} {H : Type u_3} [Zero R] [Zero S] [AddZeroClass H] {N : H →+ ℝ} (a : NovikovSeries R H N) (b : NovikovSeries S H N) (h : H) : {p : H × H | p.1 + p.2 = h ∧ a.coeff p.1 ≠ 0 ∧ b.coeff p.2 ≠ 0}.Finite

For Novikov series a and b and an exponent h, only finitely many pairs (u, v) with u + v = h have both coefficients a.coeff u and b.coeff v nonzero.

theorem TauCeti.NovikovSeries.finite_setOf_add_eq_mul_ne_zero {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} {R : Type u_4} [MulZeroClass R] (a b : NovikovSeries R H N) (h : H) : {p : H × H | p.1 + p.2 = h ∧ a.coeff p.1 * b.coeff p.2 ≠ 0}.Finite

For Novikov series a and b and an exponent h, only finitely many pairs (u, v) with u + v = h have nonzero coefficient product a.coeff u * b.coeff v.

theorem TauCeti.NovikovSeries.finite_setOf_period_add_add_lt {R : Type u_1} {S : Type u_2} {H : Type u_3} [Zero R] [Zero S] [AddZeroClass H] {N : H →+ ℝ} {T : Type u_4} [Zero T] (a : NovikovSeries R H N) (b : NovikovSeries S H N) (c : NovikovSeries T H N) (C : ℝ) : {t : H × H × H | N (t.1 + t.2.1 + t.2.2) < C ∧ a.coeff t.1 ≠ 0 ∧ b.coeff t.2.1 ≠ 0 ∧ c.coeff t.2.2 ≠ 0}.Finite

Uniform cutoff finiteness for triple products: for Novikov series a, b and c, only finitely many triples (u, v, w) of support exponents have N (u + v + w) < C.

theorem TauCeti.NovikovSeries.finite_setOf_add_add_eq {R : Type u_1} {S : Type u_2} {H : Type u_3} [Zero R] [Zero S] [AddZeroClass H] {N : H →+ ℝ} {T : Type u_4} [Zero T] (a : NovikovSeries R H N) (b : NovikovSeries S H N) (c : NovikovSeries T H N) (h : H) : {t : H × H × H | t.1 + t.2.1 + t.2.2 = h ∧ a.coeff t.1 ≠ 0 ∧ b.coeff t.2.1 ≠ 0 ∧ c.coeff t.2.2 ≠ 0}.Finite

For Novikov series a, b and c and an exponent h, only finitely many triples (u, v, w) with u + v + w = h have all three coefficients nonzero.

@[instance_reducible]

instance TauCeti.NovikovSeries.instSMul {R : Type u_1} {S : Type u_2} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [SMulZeroClass S R] : SMul S (NovikovSeries R H N)

Coefficientwise scalar multiplication of a Novikov series.

@[simp]

theorem TauCeti.NovikovSeries.coeff_smul' {R : Type u_1} {S : Type u_2} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [SMulZeroClass S R] (s : S) (a : NovikovSeries R H N) : (s • a).coeff = s • a.coeff

theorem TauCeti.NovikovSeries.coeff_smul {R : Type u_1} {S : Type u_2} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [SMulZeroClass S R] (s : S) (a : NovikovSeries R H N) (h : H) : (s • a).coeff h = s • a.coeff h

theorem TauCeti.NovikovSeries.support_smul_subset {R : Type u_1} {S : Type u_2} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [SMulZeroClass S R] (s : S) (a : NovikovSeries R H N) : (s • a).support ⊆ a.support

@[instance_reducible]

instance TauCeti.NovikovSeries.instAdd {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] : Add (NovikovSeries R H N)

Coefficientwise addition of Novikov series.

@[simp]

theorem TauCeti.NovikovSeries.coeff_add' {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] (a b : NovikovSeries R H N) : (a + b).coeff = a.coeff + b.coeff

theorem TauCeti.NovikovSeries.coeff_add {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] (a b : NovikovSeries R H N) (h : H) : (a + b).coeff h = a.coeff h + b.coeff h

theorem TauCeti.NovikovSeries.support_add_subset {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] (a b : NovikovSeries R H N) : (a + b).support ⊆ a.support ∪ b.support

@[instance_reducible]

instance TauCeti.NovikovSeries.instAddMonoid {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] : AddMonoid (NovikovSeries R H N)

@[instance_reducible]

instance TauCeti.NovikovSeries.instAddCommMonoid {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddCommMonoid R] : AddCommMonoid (NovikovSeries R H N)

@[instance_reducible]

instance TauCeti.NovikovSeries.instNeg {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NegZeroClass R] : Neg (NovikovSeries R H N)

Coefficientwise negation of a Novikov series.

@[simp]

theorem TauCeti.NovikovSeries.coeff_neg' {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NegZeroClass R] (a : NovikovSeries R H N) : (-a).coeff = -a.coeff

theorem TauCeti.NovikovSeries.coeff_neg {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NegZeroClass R] (a : NovikovSeries R H N) (h : H) : (-a).coeff h = -a.coeff h

@[instance_reducible]

instance TauCeti.NovikovSeries.instSub {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] : Sub (NovikovSeries R H N)

Coefficientwise subtraction of Novikov series.

@[simp]

theorem TauCeti.NovikovSeries.coeff_sub' {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (a b : NovikovSeries R H N) : (a - b).coeff = a.coeff - b.coeff

theorem TauCeti.NovikovSeries.coeff_sub {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (a b : NovikovSeries R H N) (h : H) : (a - b).coeff h = a.coeff h - b.coeff h

@[simp]

theorem TauCeti.NovikovSeries.support_neg {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (a : NovikovSeries R H N) : (-a).support = a.support

theorem TauCeti.NovikovSeries.support_sub_subset {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (a b : NovikovSeries R H N) : (a - b).support ⊆ a.support ∪ b.support

@[instance_reducible]

instance TauCeti.NovikovSeries.instAddGroup {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] : AddGroup (NovikovSeries R H N)

@[instance_reducible]

instance TauCeti.NovikovSeries.instAddCommGroup {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : AddCommGroup (NovikovSeries R H N)

def TauCeti.NovikovSeries.coeffAddMonoidHom {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] : NovikovSeries R H N →+ H → R

The coefficient function of Novikov series, as an additive monoid homomorphism.

@[simp]

theorem TauCeti.NovikovSeries.coeffAddMonoidHom_apply {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] (a : NovikovSeries R H N) : coeffAddMonoidHom a = a.coeff

instance TauCeti.NovikovSeries.instIsAddTorsionFree {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] [IsAddTorsionFree R] : IsAddTorsionFree (NovikovSeries R H N)

Novikov series inherit the absence of additive torsion from their coefficients.

@[simp]

theorem TauCeti.NovikovSeries.coeff_sum {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [AddCommMonoid R] {ι : Type u_4} (s : Finset ι) (f : ι → NovikovSeries R H N) (h : H) : (∑ i ∈ s, f i).coeff h = ∑ i ∈ s, (f i).coeff h

A coefficient of a finite sum of Novikov series is the sum of the coefficients.

@[instance_reducible]

instance TauCeti.NovikovSeries.instModule {R : Type u_1} {S : Type u_2} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Semiring S] [AddCommMonoid R] [Module S R] : Module S (NovikovSeries R H N)

def TauCeti.NovikovSeries.ofFinsupp {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] : (H →₀ R) →+ NovikovSeries R H N

A finitely supported coefficient function, viewed as a Novikov series.

@[simp]

theorem TauCeti.NovikovSeries.coeff_ofFinsupp {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] (f : H →₀ R) : (ofFinsupp f).coeff = ⇑f

@[simp]

theorem TauCeti.NovikovSeries.support_ofFinsupp {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] (f : H →₀ R) : (ofFinsupp f).support = ↑f.support

@[simp]

theorem TauCeti.NovikovSeries.ofFinsupp_smul {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] {S : Type u_3} [SMulZeroClass S R] (s : S) (f : H →₀ R) : ofFinsupp (s • f) = s • ofFinsupp f

theorem TauCeti.NovikovSeries.ofFinsupp_injective {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] : Function.Injective ⇑ofFinsupp

theorem TauCeti.NovikovSeries.mem_range_ofFinsupp_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] {a : NovikovSeries R H N} : a ∈ Set.range ⇑ofFinsupp ↔ a.support.Finite

noncomputable def TauCeti.NovikovSeries.single {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (h : H) (r : R) : NovikovSeries R H N

The monomial r e^h: the Novikov series with coefficient r at h and 0 elsewhere.

theorem TauCeti.NovikovSeries.coeff_single {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [DecidableEq H] (h : H) (r : R) : (single h r).coeff = Pi.single h r

@[simp]

theorem TauCeti.NovikovSeries.coeff_single_same {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (h : H) (r : R) : (single h r).coeff h = r

@[simp]

theorem TauCeti.NovikovSeries.coeff_single_of_ne {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {g h : H} (hgh : g ≠ h) (r : R) : (single h r).coeff g = 0

theorem TauCeti.NovikovSeries.support_single_subset {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (h : H) (r : R) : (single h r).support ⊆ {h}

@[simp]

theorem TauCeti.NovikovSeries.support_single_of_ne {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {h : H} {r : R} (hr : r ≠ 0) : (single h r).support = {h}

@[simp]

theorem TauCeti.NovikovSeries.single_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (h : H) : single h 0 = 0

theorem TauCeti.NovikovSeries.single_injective {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (h : H) : Function.Injective (single h)

@[simp]

theorem TauCeti.NovikovSeries.single_eq_zero_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {h : H} {r : R} : single h r = 0 ↔ r = 0

instance TauCeti.NovikovSeries.instNontrivial {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [Nontrivial R] : Nontrivial (NovikovSeries R H N)

@[simp]

theorem TauCeti.NovikovSeries.single_zero_coeff_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [Subsingleton H] (a : NovikovSeries R H N) : single 0 (a.coeff 0) = a

Over a trivial exponent group every Novikov series is the constant monomial of its coefficient at 0.

@[simp]

theorem TauCeti.NovikovSeries.single_add {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] (h : H) (r s : R) : single h (r + s) = single h r + single h s

@[simp]

theorem TauCeti.NovikovSeries.single_neg {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NegZeroClass R] (h : H) (r : R) : single h (-r) = -single h r

@[simp]

theorem TauCeti.NovikovSeries.single_sub {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (h : H) (r s : R) : single h (r - s) = single h r - single h s

theorem TauCeti.NovikovSeries.smul_single {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} {S : Type u_3} [Zero R] [SMulZeroClass S R] (s : S) (h : H) (r : R) : s • single h r = single h (s • r)

@[simp]

theorem TauCeti.NovikovSeries.ofFinsupp_single {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] (h : H) (r : R) : ofFinsupp (Finsupp.single h r) = single h r

noncomputable def TauCeti.NovikovSeries.order {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (a : NovikovSeries R H N) : ℝ

The order of a Novikov series: the least period of its support, and 0 for the zero series.

@[simp]

theorem TauCeti.NovikovSeries.order_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] : order 0 = 0

theorem TauCeti.NovikovSeries.isLeast_order {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {a : NovikovSeries R H N} (ha : a ≠ 0) : IsLeast (⇑N '' a.support) a.order

The order of a nonzero Novikov series is the least period of its support.

theorem TauCeti.NovikovSeries.order_eq_of_isLeast {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {a : NovikovSeries R H N} {C : ℝ} (hC : IsLeast (⇑N '' a.support) C) : a.order = C

A Novikov series whose support has least period C has order C.

theorem TauCeti.NovikovSeries.order_le_of_coeff_ne_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {a : NovikovSeries R H N} {h : H} (hh : a.coeff h ≠ 0) : a.order ≤ N h

theorem TauCeti.NovikovSeries.coeff_eq_zero_of_lt_order {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {a : NovikovSeries R H N} {h : H} (hh : N h < a.order) : a.coeff h = 0

theorem TauCeti.NovikovSeries.exists_coeff_ne_zero_and_period_eq_order {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {a : NovikovSeries R H N} (ha : a ≠ 0) : ∃ (h : H), a.coeff h ≠ 0 ∧ N h = a.order

A nonzero Novikov series has a nonzero coefficient at an exponent of period equal to its order.

theorem TauCeti.NovikovSeries.le_order_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {a : NovikovSeries R H N} {C : ℝ} (ha : a ≠ 0) : C ≤ a.order ↔ ∀ (h : H), N h < C → a.coeff h = 0

A nonzero Novikov series vanishes below the period cutoff C exactly when C is at most its order.

@[simp]

theorem TauCeti.NovikovSeries.order_single {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] {h : H} {r : R} (hr : r ≠ 0) : (single h r).order = N h

theorem TauCeti.NovikovSeries.min_order_le_order_add {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] {a b : NovikovSeries R H N} (hab : a + b ≠ 0) : min a.order b.order ≤ (a + b).order

The order of a nonzero sum is at least the smaller of the orders of the summands.

@[simp]

theorem TauCeti.NovikovSeries.order_neg {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (a : NovikovSeries R H N) : (-a).order = a.order

noncomputable def TauCeti.NovikovSeries.trunc {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (C : ℝ) (a : NovikovSeries R H N) : H →₀ R

The truncation of a Novikov series a below the period cutoff C: the finitely supported coefficient function that agrees with a at exponents of period < C and vanishes elsewhere.

@[simp]

theorem TauCeti.NovikovSeries.trunc_apply {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (C : ℝ) (a : NovikovSeries R H N) (h : H) : (trunc C a) h = if N h < C then a.coeff h else 0

theorem TauCeti.NovikovSeries.trunc_apply_of_lt {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} {C : ℝ} [Zero R] {a : NovikovSeries R H N} {h : H} (hh : N h < C) : (trunc C a) h = a.coeff h

theorem TauCeti.NovikovSeries.trunc_apply_of_le {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} {C : ℝ} [Zero R] {a : NovikovSeries R H N} {h : H} (hh : C ≤ N h) : (trunc C a) h = 0

@[simp]

theorem TauCeti.NovikovSeries.trunc_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Zero R] (C : ℝ) : trunc C 0 = 0

@[simp]

theorem TauCeti.NovikovSeries.trunc_add {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddZeroClass R] (C : ℝ) (a b : NovikovSeries R H N) : trunc C (a + b) = trunc C a + trunc C b

@[simp]

theorem TauCeti.NovikovSeries.trunc_neg {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NegZeroClass R] (C : ℝ) (a : NovikovSeries R H N) : trunc C (-a) = -trunc C a

@[simp]

theorem TauCeti.NovikovSeries.trunc_sub {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (C : ℝ) (a b : NovikovSeries R H N) : trunc C (a - b) = trunc C a - trunc C b

@[simp]

theorem TauCeti.NovikovSeries.trunc_smul {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} {S : Type u_3} [Zero R] [SMulZeroClass S R] (C : ℝ) (s : S) (a : NovikovSeries R H N) : trunc C (s • a) = s • trunc C a

theorem TauCeti.NovikovSeries.ofFinsupp_surjective_iff {R : Type u_1} {H : Type u_2} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [Nontrivial R] : Function.Surjective ⇑ofFinsupp ↔ N = 0

Over a nontrivial coefficient type, every Novikov series is finitely supported if and only if the period homomorphism vanishes.