Right division in a coefficient-left derivation Ore model

This file is the next structural layer after ore_derivation.lean. It does not identify a presented Weyl algebra with this model. It builds the finite normal-form algebra needed for that identification: the normal form of x^i * b, the right product of a normal polynomial by a monomial b*x^j, and the leading-term fact which drives right division by a monic polynomial.

The coefficient ring is allowed to be noncommutative. No commutative polynomial division theorem is used.

structure AlgebraicAnalysis.OreDivisionDerivation (B : Type u_1) [Ring B] : Type u_1

A derivation used to define a coefficient-left Ore normal form.

• toFun : B → B

  The underlying additive derivation map.

• map_zero' : self.toFun 0 = 0

  The derivation preserves zero.

• map_add' (a b : B) : self.toFun (a + b) = self.toFun a + self.toFun b

  The derivation preserves addition.

• leibniz' (a b : B) : self.toFun (a * b) = a * self.toFun b + self.toFun a * b

  The Leibniz rule.

@[instance_reducible]

instance AlgebraicAnalysis.instCoeFunOreDivisionDerivationForall {B : Type u_1} [Ring B] : CoeFun (OreDivisionDerivation B) fun (x : OreDivisionDerivation B) => B → B

Equations

• AlgebraicAnalysis.instCoeFunOreDivisionDerivationForall = { coe := AlgebraicAnalysis.OreDivisionDerivation.toFun }

@[simp]

theorem AlgebraicAnalysis.OreDivisionDerivation.map_zero {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) : D.toFun 0 = 0

@[simp]

theorem AlgebraicAnalysis.OreDivisionDerivation.map_add {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (a b : B) : D.toFun (a + b) = D.toFun a + D.toFun b

@[simp]

theorem AlgebraicAnalysis.OreDivisionDerivation.leibniz {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (a b : B) : D.toFun (a * b) = a * D.toFun b + D.toFun a * b

theorem AlgebraicAnalysis.OreDivisionDerivation.map_nsmul {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (a : B) (n : ℕ) : D.toFun (n • a) = n • D.toFun a

noncomputable def AlgebraicAnalysis.OreDivision.push {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (i : ℕ) : Polynomial B

The coefficient-left normal form of x^i*b under x*b=b*x+D(b).

Equations

• AlgebraicAnalysis.OreDivision.push D b i = ∑ k ∈ Finset.range (i + 1), (Polynomial.monomial (i - k)) (i.choose k • D.toFun^[k] b)

theorem AlgebraicAnalysis.OreDivision.push_coeff {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (i n : ℕ) : (push D b i).coeff n = ∑ k ∈ Finset.range (i + 1), if i - k = n then i.choose k • D.toFun^[k] b else 0

theorem AlgebraicAnalysis.OreDivision.push_degree_le {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (i : ℕ) : (push D b i).degree ≤ ↑i

theorem AlgebraicAnalysis.OreDivision.push_coeff_top {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (i : ℕ) : (push D b i).coeff i = b

theorem AlgebraicAnalysis.OreDivision.push_eq_zero_of {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (i : ℕ) (h : b = 0) : push D b i = 0

noncomputable def AlgebraicAnalysis.OreDivision.rightTerm {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (i : ℕ) (a b : B) (j : ℕ) : Polynomial B

Right multiplication of a normal polynomial by the monomial b*x^j.

The definition is coefficientwise and finite. It is deliberately not the ordinary multiplication of Polynomial B: the inner push expansion is the derivation correction for moving b through powers of x.

Equations

• AlgebraicAnalysis.OreDivision.rightTerm D i a b j = ∑ k ∈ Finset.range (i + 1), (Polynomial.monomial (i - k + j)) (a * i.choose k • D.toFun^[k] b)

noncomputable def AlgebraicAnalysis.OreDivision.rightMulMonomial {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (b : B) (j : ℕ) : Polynomial B

Right multiplication by one coefficient-monomial.

Equations

• AlgebraicAnalysis.OreDivision.rightMulMonomial D p b j = p.sum fun (i : ℕ) (a : B) => AlgebraicAnalysis.OreDivision.rightTerm D i a b j

theorem AlgebraicAnalysis.OreDivision.rightMulMonomial_coeff {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (b : B) (j n : ℕ) : (rightMulMonomial D p b j).coeff n = ∑ i ∈ p.support, ∑ k ∈ Finset.range (i + 1), if i - k + j = n then p.coeff i * i.choose k • D.toFun^[k] b else 0

theorem AlgebraicAnalysis.OreDivision.rightTerm_zero {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (i : ℕ) (b : B) (j : ℕ) : rightTerm D i 0 b j = 0

theorem AlgebraicAnalysis.OreDivision.rightTerm_add_left {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (i : ℕ) (a₁ a₂ b : B) (j : ℕ) : rightTerm D i (a₁ + a₂) b j = rightTerm D i a₁ b j + rightTerm D i a₂ b j

theorem AlgebraicAnalysis.OreDivision.rightMulMonomial_add_left {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p q : Polynomial B) (b : B) (j : ℕ) : rightMulMonomial D (p + q) b j = rightMulMonomial D p b j + rightMulMonomial D q b j

theorem AlgebraicAnalysis.OreDivision.iterate_add {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) (b₁ b₂ : B) : D.toFun^[n] (b₁ + b₂) = D.toFun^[n] b₁ + D.toFun^[n] b₂

theorem AlgebraicAnalysis.OreDivision.iterate_zero {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : D.toFun^[n] 0 = 0

theorem AlgebraicAnalysis.OreDivision.rightMulMonomial_add_right {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (b₁ b₂ : B) (j : ℕ) : rightMulMonomial D p (b₁ + b₂) j = rightMulMonomial D p b₁ j + rightMulMonomial D p b₂ j

theorem AlgebraicAnalysis.OreDivision.rightMulMonomial_zero_right {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (j : ℕ) : rightMulMonomial D p 0 j = 0

noncomputable def AlgebraicAnalysis.OreDivision.rightMul {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d q : Polynomial B) : Polynomial B

The product d*q of a normal polynomial by a normal right quotient.

Equations

• AlgebraicAnalysis.OreDivision.rightMul D d q = q.sum fun (j : ℕ) (c : B) => AlgebraicAnalysis.OreDivision.rightMulMonomial D d c j

theorem AlgebraicAnalysis.OreDivision.rightMul_add {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d q₁ q₂ : Polynomial B) : rightMul D d (q₁ + q₂) = rightMul D d q₁ + rightMul D d q₂

theorem AlgebraicAnalysis.OreDivision.rightMul_zero {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d : Polynomial B) : rightMul D d 0 = 0

noncomputable def AlgebraicAnalysis.OreDivision.rightMulAddHom {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d : Polynomial B) : Polynomial B →+ Polynomial B

The additive map given by right multiplication by a fixed normal form.

Equations

• AlgebraicAnalysis.OreDivision.rightMulAddHom D d = { toFun := AlgebraicAnalysis.OreDivision.rightMul D d, map_zero' := ⋯, map_add' := ⋯ }

theorem AlgebraicAnalysis.OreDivision.rightMul_sub {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d q₁ q₂ : Polynomial B) : rightMul D d (q₁ - q₂) = rightMul D d q₁ - rightMul D d q₂

theorem AlgebraicAnalysis.OreDivision.rightMul_monomial {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d : Polynomial B) (c : B) (j : ℕ) : rightMul D d ((Polynomial.monomial j) c) = rightMulMonomial D d c j

theorem AlgebraicAnalysis.OreDivision.rightMulMonomial_degree_le {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (b : B) (j : ℕ) : (rightMulMonomial D p b j).degree ≤ ↑p.natDegree + ↑j

theorem AlgebraicAnalysis.OreDivision.rightMulMonomial_coeff_top {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (hp : p ≠ 0) (b : B) (j : ℕ) : (rightMulMonomial D p b j).coeff (p.natDegree + j) = p.leadingCoeff * b

theorem AlgebraicAnalysis.OreDivision.rightMul_degree_le {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (d q : Polynomial B) : (rightMul D d q).degree ≤ ↑d.natDegree + ↑q.natDegree

theorem AlgebraicAnalysis.OreDivision.rightMul_coeff_top {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d q : Polynomial B) (hd : d.Monic) (hq : q ≠ 0) : (rightMul D d q).coeff (d.natDegree + q.natDegree) = q.leadingCoeff

theorem AlgebraicAnalysis.OreDivision.rightMul_degree_eq {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d q : Polynomial B) (hd : d.Monic) (hq : q ≠ 0) : (rightMul D d q).degree = ↑d.natDegree + ↑q.natDegree

theorem AlgebraicAnalysis.OreDivision.rightMul_injective {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d : Polynomial B) (hd : d.Monic) : Function.Injective (rightMul D d)

The leading-degree theorem packages the strict filtered-intersection property needed by the relative principal-source construction. This is an Ore-polynomial filtration statement; it is deliberately not identified here with the Bernstein filtration on the Weyl algebra.

theorem AlgebraicAnalysis.OreDivision.rightMul_degree_le_iff {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d q : Polynomial B) (hd : d.Monic) (n : ℕ) : (rightMul D d q).degree ≤ ↑n ↔ q = 0 ∨ d.natDegree + q.natDegree ≤ n

theorem AlgebraicAnalysis.OreDivision.remainder_degree_lt {B : Type u_1} [Ring B] (d r : Polynomial B) (hr : r = 0 ∨ r.natDegree < d.natDegree) : r.degree < ↑d.natDegree

theorem AlgebraicAnalysis.OreDivision.right_division_unique {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d p q₁ q₂ r₁ r₂ : Polynomial B) (hd : d.Monic) (h₁ : p = rightMul D d q₁ + r₁) (h₂ : p = rightMul D d q₂ + r₂) (hr₁ : r₁ = 0 ∨ r₁.natDegree < d.natDegree) (hr₂ : r₂ = 0 ∨ r₂.natDegree < d.natDegree) : q₁ = q₂ ∧ r₁ = r₂

theorem AlgebraicAnalysis.OreDivision.cancel_degree_lt {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d p : Polynomial B) (hd : d.Monic) (hp : p ≠ 0) (hdeg : d.natDegree ≤ p.natDegree) : (p - rightMulMonomial D d p.leadingCoeff (p.natDegree - d.natDegree)).degree < p.degree

theorem AlgebraicAnalysis.OreDivision.right_division_exists {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) [Nontrivial B] (d p : Polynomial B) (hd : d.Monic) : ∃ (q : Polynomial B) (r : Polynomial B), p = rightMul D d q + r ∧ (r = 0 ∨ r.natDegree < d.natDegree)

structure AlgebraicAnalysis.OreDivision.OreAmbient (B : Type u_2) (A : Type u_3) [Ring B] [Ring A] (D : OreDivisionDerivation B) : Type (max u_2 u_3)

An ambient ring in which the Ore relation is represented.

• embed : B →+* A

  The coefficient-ring embedding.

• x : A

  The element representing the Ore variable.

• relation (b : B) : self.x * self.embed b = self.embed b * self.x + self.embed (D.toFun b)

  The defining relation in the ambient ring.

def AlgebraicAnalysis.OreDivision.OreAmbient.commutatorDerivation {A : Type u_3} [Ring A] (p : A) : OreDivisionDerivation A

The inner derivation a ↦ p*a-a*p, used to formalize the iterated commutator expansion of a power of p.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.commutatorDerivation p = { toFun := fun (a : A) => p * a - a * p, map_zero' := ⋯, map_add' := ⋯, leibniz' := ⋯ }

def AlgebraicAnalysis.OreDivision.OreAmbient.commutatorAmbient {A : Type u_3} [Ring A] (p : A) : OreAmbient A A (commutatorDerivation p)

The ambient Ore presentation for an inner derivation.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.commutatorAmbient p = { embed := RingHom.id A, x := p, relation := ⋯ }

def AlgebraicAnalysis.OreDivision.OreAmbient.term {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (i j : ℕ) : A

A term in the iterated commutator expansion.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.term D O b i j = O.embed (D.toFun^[i] b) * O.x ^ j

theorem AlgebraicAnalysis.OreDivision.OreAmbient.push_term {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (i j : ℕ) : O.x * term D O b i j = term D O b i (j + 1) + term D O b (i + 1) j

theorem AlgebraicAnalysis.OreDivision.OreAmbient.mul_nsmul_left {A : Type u_3} [Ring A] (a u : A) (n : ℕ) : a * n • u = n • (a * u)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.nsmul_mul_right {A : Type u_3} [Ring A] (a u : A) (n : ℕ) : n • a * u = n • (a * u)

def AlgebraicAnalysis.OreDivision.OreAmbient.expansion {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (n : ℕ) : A

The normal-order expansion of x^n * embed b.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.expansion D O b n = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • AlgebraicAnalysis.OreDivision.OreAmbient.term D O b ij.1 ij.2

theorem AlgebraicAnalysis.OreDivision.OreAmbient.pow_mul {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (n : ℕ) : O.x ^ n * O.embed b = expansion D O b n

def AlgebraicAnalysis.OreDivision.OreAmbient.reverseTerm {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (i j : ℕ) : A

A single coefficient moved through a power of the Ore variable.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.reverseTerm D O b i j = O.x ^ j * O.embed (D.toFun^[i] b)

def AlgebraicAnalysis.OreDivision.OreAmbient.reverseSignedTerm {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (i j : ℕ) : A

A signed term for the reverse normal-order expansion.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.reverseSignedTerm D O b i j = (-1) ^ i * AlgebraicAnalysis.OreDivision.OreAmbient.reverseTerm D O b i j

def AlgebraicAnalysis.OreDivision.OreAmbient.reverseExpansion {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (n : ℕ) : A

The reverse normal-order expansion of x^n * embed b.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.reverseExpansion D O b n = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • AlgebraicAnalysis.OreDivision.OreAmbient.reverseSignedTerm D O b ij.1 ij.2

theorem AlgebraicAnalysis.OreDivision.OreAmbient.reverseTerm_mul {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (i j : ℕ) : reverseTerm D O b i j * O.x = reverseTerm D O b i (j + 1) - reverseTerm D O b (i + 1) j

theorem AlgebraicAnalysis.OreDivision.OreAmbient.reverseSignedTerm_mul {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (i j : ℕ) : reverseSignedTerm D O b i j * O.x = reverseSignedTerm D O b i (j + 1) + reverseSignedTerm D O b (i + 1) j

theorem AlgebraicAnalysis.OreDivision.OreAmbient.reverse_mul {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (n : ℕ) : O.embed b * O.x ^ n = reverseExpansion D O b n

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_pow_mul {A : Type u_3} [Ring A] (p a : A) (m : ℕ) : p ^ m * a = expansion (commutatorDerivation p) (commutatorAmbient p) a m

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_pow_mul_explicit {A : Type u_3} [Ring A] (p a : A) (m : ℕ) : p ^ m * a = ∑ ij ∈ Finset.antidiagonal m, m.choose ij.1 • ((commutatorDerivation p).toFun^[ij.1] a * p ^ ij.2)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_pow_succ {A : Type u_3} [Ring A] (p x : A) (hpx : p * x - x * p = 1) (r : ℕ) : p * x ^ (r + 1) - x ^ (r + 1) * p = (r + 1) • x ^ r

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_pow_of_le {A : Type u_3} [Ring A] (p x : A) (hpx : p * x - x * p = 1) (j n : ℕ) (hjn : j ≤ n) : (commutatorDerivation p).toFun^[j] (x ^ n) = n.descFactorial j • x ^ (n - j)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_pow_of_lt {A : Type u_3} [Ring A] (p x : A) (hpx : p * x - x * p = 1) (j n : ℕ) (hnj : n < j) : (commutatorDerivation p).toFun^[j] (x ^ n) = 0

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_pow {A : Type u_3} [Ring A] (p x : A) (hpx : p * x - x * p = 1) (j n : ℕ) : (commutatorDerivation p).toFun^[j] (x ^ n) = if j ≤ n then n.descFactorial j • x ^ (n - j) else 0

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_pow_mul_pow {A : Type u_3} [Ring A] (p x : A) (hpx : p * x - x * p = 1) (k r : ℕ) : p ^ k * x ^ r = ∑ i ∈ Finset.range (k + 1), if i ≤ r then (k.choose i * r.descFactorial i) • (x ^ (r - i) * p ^ (k - i)) else 0

p-free monic corner

The quotient by the image of right multiplication by p keeps only the p-free term of the normal-ordering expansion. The following theorem isolates the monic contribution; lower coefficient terms are handled by the separate Newton arithmetic lemmas in a2_newton_bound.lean.

def AlgebraicAnalysis.OreDivision.OreAmbient.pRightMulLinear {k : Type u_4} {A : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] (p : A) : A →ₗ[k] A

The linear map given by right multiplication by p.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.pRightMulLinear p = LinearMap.mulRight k p

def AlgebraicAnalysis.OreDivision.OreAmbient.pRightMulRange {k : Type u_4} {A : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] (p : A) : Submodule k A

The range of right multiplication by p.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.pRightMulRange p = (AlgebraicAnalysis.OreDivision.OreAmbient.pRightMulLinear p).range

theorem AlgebraicAnalysis.OreDivision.OreAmbient.pRightMulRange_mem_of_mul_p {k : Type u_4} {A : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] (p z : A) : z * p ∈ pRightMulRange p

theorem AlgebraicAnalysis.OreDivision.OreAmbient.pfree_power_of_le {k : Type u_4} {A : Type u_5} [Field k] [Ring A] [Algebra k A] (p x : A) (hpx : p * x - x * p = 1) (u n : ℕ) (hun : u ≤ n) : (pRightMulRange p).mkQ (p ^ u * x ^ n) = ↑(n.descFactorial u) • (pRightMulRange p).mkQ (x ^ (n - u))

theorem AlgebraicAnalysis.OreDivision.OreAmbient.pfree_monic_corner {k : Type u_4} {A : Type u_5} [Field k] [Ring A] [Algebra k A] (p x : A) (hpx : p * x - x * p = 1) (m r : ℕ) : (pRightMulRange p).mkQ (p ^ m * x ^ (m + r)) = (↑(m.choose m) * ↑((m + r).descFactorial m)) • (pRightMulRange p).mkQ (x ^ r)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutatorDerivation_mul_left {A : Type u_3} [Ring A] (p b y : A) (hpb : p * b = b * p) : (commutatorDerivation p).toFun (b * y) = b * (commutatorDerivation p).toFun y

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_mul_left {A : Type u_3} [Ring A] (p b y : A) (hpb : p * b = b * p) (j : ℕ) : (commutatorDerivation p).toFun^[j] (b * y) = b * (commutatorDerivation p).toFun^[j] y

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_add {A : Type u_3} [Ring A] (p : A) (j : ℕ) (a b : A) : (commutatorDerivation p).toFun^[j] (a + b) = (commutatorDerivation p).toFun^[j] a + (commutatorDerivation p).toFun^[j] b

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_sum {A : Type u_3} [Ring A] (p : A) (j : ℕ) (s : Finset ℕ) (f : ℕ → A) : (commutatorDerivation p).toFun^[j] (∑ i ∈ s, f i) = ∑ i ∈ s, (commutatorDerivation p).toFun^[j] (f i)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_eval_monomial_of_le {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p b : B) (n j : ℕ) (hpb : ∀ (c : B), O.embed p * O.embed c = O.embed c * O.embed p) (hDp : D.toFun p = -1) (hjn : j ≤ n) : (commutatorDerivation (O.embed p)).toFun^[j] (O.embed b * O.x ^ n) = O.embed b * n.descFactorial j • O.x ^ (n - j)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_eval_monomial {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p b : B) (n j : ℕ) (hpb : ∀ (c : B), O.embed p * O.embed c = O.embed c * O.embed p) (hDp : D.toFun p = -1) : (commutatorDerivation (O.embed p)).toFun^[j] (O.embed b * O.x ^ n) = if j ≤ n then O.embed b * n.descFactorial j • O.x ^ (n - j) else 0

def AlgebraicAnalysis.OreDivision.OreAmbient.eval {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p : Polynomial B) : A

Evaluation of a normal polynomial in an ambient Ore ring.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.eval D O p = p.sum fun (i : ℕ) (b : B) => O.embed b * O.x ^ i

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_eval {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p : A) (q : Polynomial B) (j : ℕ) : (commutatorDerivation p).toFun^[j] (eval D O q) = ∑ i ∈ q.support, (commutatorDerivation p).toFun^[j] (O.embed (q.coeff i) * O.x ^ i)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_zero {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) : eval D O 0 = 0

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_add {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p q : Polynomial B) : eval D O (p + q) = eval D O p + eval D O q

def AlgebraicAnalysis.OreDivision.OreAmbient.evalAddHom {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) : Polynomial B →+ A

The additive evaluation homomorphism.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.evalAddHom D O = { toFun := AlgebraicAnalysis.OreDivision.OreAmbient.eval D O, map_zero' := ⋯, map_add' := ⋯ }

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_monomial {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (j : ℕ) : eval D O ((Polynomial.monomial j) b) = O.embed b * O.x ^ j

noncomputable def AlgebraicAnalysis.OreDivision.OreAmbient.commutatorNormal {B : Type u_2} [Ring B] (q : Polynomial B) (j : ℕ) : Polynomial B

The coefficient-left normal form of an iterated commutator.

Equations

• AlgebraicAnalysis.OreDivision.OreAmbient.commutatorNormal q j = ∑ i ∈ q.support, if j ≤ i then (Polynomial.monomial (i - j)) (i.descFactorial j • q.coeff i) else 0

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutatorNormal_degree_le {B : Type u_2} [Ring B] (q : Polynomial B) (j : ℕ) : (commutatorNormal q j).degree ≤ ↑(q.natDegree - j)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutatorNormal_coeff_top {B : Type u_2} [Ring B] [Nontrivial B] (q : Polynomial B) (j : ℕ) (hq : q.Monic) (hjn : j ≤ q.natDegree) : (commutatorNormal q j).coeff (q.natDegree - j) = q.natDegree.descFactorial j • 1

theorem AlgebraicAnalysis.OreDivision.OreAmbient.commutator_iterate_eval_eq_eval_normal {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p : B) (q : Polynomial B) (j : ℕ) (hpb : ∀ (c : B), O.embed p * O.embed c = O.embed c * O.embed p) (hDp : D.toFun p = -1) : (commutatorDerivation (O.embed p)).toFun^[j] (eval D O q) = eval D O (commutatorNormal q j)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_push_eq_expansion {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (n : ℕ) : eval D O (push D b n) = expansion D O b n

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_push {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (b : B) (n : ℕ) : eval D O (push D b n) = O.x ^ n * O.embed b

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_rightTerm {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (i : ℕ) (a b : B) (j : ℕ) : eval D O (rightTerm D i a b j) = O.embed a * O.x ^ i * (O.embed b * O.x ^ j)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_rightMulMonomial {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (p : Polynomial B) (b : B) (j : ℕ) : eval D O (rightMulMonomial D p b j) = eval D O p * (O.embed b * O.x ^ j)

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_rightMul {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) (d q : Polynomial B) : eval D O (rightMul D d q) = eval D O d * eval D O q

theorem AlgebraicAnalysis.OreDivision.OreAmbient.eval_right_division_sound {B : Type u_2} {A : Type u_3} [Ring B] [Ring A] (D : OreDivisionDerivation B) (O : OreAmbient B A D) [Nontrivial B] (d p : Polynomial B) (hd : d.Monic) : ∃ (q : Polynomial B) (r : Polynomial B), eval D O p = eval D O d * eval D O q + eval D O r ∧ (r = 0 ∨ r.natDegree < d.natDegree)