Diagonal Laurent-coefficient Hahn series

DefinitionDiagonal Laurent-coefficient Hahn series#✓fully proved

The Hahn series with coefficient c y at inner exponent d - y and outer exponent y for every y ≥ j₀.

noncomputable def diagonalLaurentSeries {R : Type*} [CommSemiring R]
    (d : ℤ) (c : ℤ → R) (j₀ : ℤ) : HahnSeries ℤ (LaurentPolynomial R) :=
  ofSuppBddBelow
    (fun j => if j₀ ≤ j then AddMonoidAlgebra.single (d - j) (c j) else 0)
    ⟨j₀, fun j hj => by
      by_contra h
      simp [h] at hj⟩

Used by 5

Used byInverse of the variable difference as a diagonal series · Powers of the inverse variable difference have binomial coefficients · Double coefficients of a diagonal Laurent series · Outer coefficient of a diagonal Laurent series · Variable difference as a unit of Hahn series

TheoremOuter coefficient of a diagonal Laurent series#✓fully proved

The outer coefficient of a diagonal Laurent series.

@[simp] theorem coeff_diagonalLaurentSeries {R : Type*} [CommSemiring R]
    (d : ℤ) (c : ℤ → R) (j₀ y : ℤ) :
    (diagonalLaurentSeries d c j₀).coeff y =
      if j₀ ≤ y then AddMonoidAlgebra.single (d - y) (c y) else 0

Uses 1 · Used by 1

Statement usesDiagonal Laurent-coefficient Hahn series

Used byDouble coefficients of a diagonal Laurent series

TheoremDouble coefficients of a diagonal Laurent series#✓fully proved

Both coefficients of a diagonal Laurent series, exposing its cutoff and diagonal equation.

theorem coeff_coeff_diagonalLaurentSeries {R : Type*} [CommSemiring R]
    (d : ℤ) (c : ℤ → R) (j₀ x y : ℤ) :
    ((diagonalLaurentSeries d c j₀).coeff y).coeff x =
      if j₀ ≤ y ∧ x + y = d then c y else 0

Uses 2 · Used by 2

Statement usesDiagonal Laurent-coefficient Hahn series

Proof usesOuter coefficient of a diagonal Laurent series

Used byPowers of the inverse variable difference have binomial coefficients · Variable difference as a unit of Hahn series

TheoremMultiplying by the variable difference on diagonal coefficients#✓fully proved

Multiplication by the difference of the two variables takes a difference of adjacent diagonal coefficients.

theorem coeff_coeff_variableDifference_mul {R : Type*} [CommRing R]
    (f : HahnSeries ℤ (LaurentPolynomial R)) (x y : ℤ) :
    (((single 0 (T 1) - single 1 1) * f).coeff y).coeff x =
      (f.coeff y).coeff (x - 1) - (f.coeff (y - 1)).coeff x

Used by 2

Used byPowers of the inverse variable difference have binomial coefficients · Variable difference as a unit of Hahn series

DefinitionVariable difference as a unit of Hahn series#✓fully proved

The formal difference of the inner and outer variables, bundled with its diagonal-series inverse.

HahnSeries.variableDifferenceUnit · 23 lines

noncomputable def variableDifferenceUnit {R : Type*} [CommRing R] :
    (HahnSeries ℤ (LaurentPolynomial R))ˣ := by
  let v : HahnSeries ℤ (LaurentPolynomial R) := single 0 (T 1) - single 1 1
  let e : HahnSeries ℤ (LaurentPolynomial R) :=
    diagonalLaurentSeries (-1) (fun _ => 1) 0
  have h : v * e = 1 := by
    have coeff_laurent_one (z : ℤ) :
        (1 : LaurentPolynomial R).coeff z = if z = 0 then 1 else 0 := by
      rw [← T_zero]
      unfold T
      rw [AddMonoidAlgebra.coeff_single, Finsupp.single_apply]
      simp [eq_comm]
    ext y x
    change (((single 0 (T 1) - single 1 1) * e).coeff y).coeff x =
      ((1 : HahnSeries ℤ (LaurentPolynomial R)).coeff y).coeff x
    rw [coeff_coeff_variableDifference_mul]
    simp only [e, coeff_coeff_diagonalLaurentSeries, coeff_one]
    split_ifs <;> simp_all <;> omega
  exact
    { val := v
      inv := e
      val_inv := h
      inv_val := by simpa only [mul_comm] using h }

Uses 3 · Used by 3

Statement usesDouble coefficients of a diagonal Laurent series · Multiplying by the variable difference on diagonal coefficients · Diagonal Laurent-coefficient Hahn series

Used byInverse of the variable difference as a diagonal series · Powers of the inverse variable difference have binomial coefficients · Value of the variable difference unit

TheoremValue of the variable difference unit#✓fully proved

The value of variableDifferenceUnit is the difference of the two formal variables.

@[simp] theorem coe_variableDifferenceUnit {R : Type*} [CommRing R] :
    (variableDifferenceUnit (R := R) : HahnSeries ℤ (LaurentPolynomial R)) =
      single 0 (T 1) - single 1 1

Uses 1 · Used by 1

Statement usesVariable difference as a unit of Hahn series

Used byPowers of the inverse variable difference have binomial coefficients

TheoremInverse of the variable difference as a diagonal series#✓fully proved

The inverse of the formal variable difference is its infinite diagonal Laurent series.

@[simp] theorem coe_inv_variableDifferenceUnit {R : Type*} [CommRing R] :
    (↑((variableDifferenceUnit (R := R))⁻¹) : HahnSeries ℤ (LaurentPolynomial R)) =
      diagonalLaurentSeries (-1) (fun _ => 1) 0

Uses 2 · Used by 1

Statement usesDiagonal Laurent-coefficient Hahn series · Variable difference as a unit of Hahn series

Used byPowers of the inverse variable difference have binomial coefficients

TheoremPowers of the inverse variable difference have binomial coefficients#✓fully proved

The (N + 1)-st power of the inverse variable difference has negative-binomial coefficients on one diagonal.

theorem coe_inv_variableDifferenceUnit_pow_succ {R : Type*} [CommRing R] (N : ℕ) :
    (↑((variableDifferenceUnit (R := R))⁻¹) : HahnSeries ℤ (LaurentPolynomial R)) ^
        (N + 1) =
      diagonalLaurentSeries (-(N : ℤ) - 1)
        (fun j => ((j.toNat + N).choose N : R)) 0

Uses 6

Statement usesDiagonal Laurent-coefficient Hahn series · Variable difference as a unit of Hahn series

Proof usesInverse of the variable difference as a diagonal series · Value of the variable difference unit · Double coefficients of a diagonal Laurent series · Multiplying by the variable difference on diagonal coefficients

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.