Holonomic (D-finite) certificates

Lean counterpart of the Python kernel in scratch/isar_holonomic_closure_algebra.py.

structure ISAR.HolonomicCertificate : Type

Polynomial-coefficient linear ODE certificate of order order.

• order : ℕ
• coeffs : Fin (self.order + 1) → Polynomial ℝ
• leading_ne : self.coeffs ⟨self.order, ⋯⟩ ≠ 0

noncomputable def ISAR.HolonomicCertificate.residual (c : HolonomicCertificate) (f : ℝ → ℝ) (x : ℝ) : ℝ

Pointwise residual of a certificate against a function.

Equations

• c.residual f x = ∑ i : Fin (c.order + 1), Polynomial.eval x (c.coeffs i) * iteratedDeriv (↑i) f x

def ISAR.satisfiesODE (c : HolonomicCertificate) (f : ℝ → ℝ) : Prop

f satisfies the holonomic ODE encoded by c.

Equations

• ISAR.satisfiesODE c f = ∀ (x : ℝ), c.residual f x = 0

def ISAR.IsHolonomic (f : ℝ → ℝ) : Prop

f admits some holonomic certificate.

Equations

• ISAR.IsHolonomic f = ∃ (c : ISAR.HolonomicCertificate), ISAR.satisfiesODE c f

theorem ISAR.verify_certificate_iff (c : HolonomicCertificate) (f : ℝ → ℝ) : satisfiesODE c f ↔ ∀ (x : ℝ), c.residual f x = 0

theorem ISAR.cert_sound (c : HolonomicCertificate) (f : ℝ → ℝ) (h : ∀ (x : ℝ), c.residual f x = 0) : satisfiesODE c f

def ISAR.orderOneCert (p0 p1 : Polynomial ℝ) (hp1 : p1 ≠ 0) : HolonomicCertificate

Build an order-1 certificate p₀ · f + p₁ · f' = 0 with p₁ ≠ 0.

Equations

• ISAR.orderOneCert p0 p1 hp1 = { order := 1, coeffs := fun (i : Fin (1 + 1)) => if ↑i = 0 then p0 else p1, leading_ne := ⋯ }

def ISAR.orderTwoCert (p0 p1 p2 : Polynomial ℝ) (hp2 : p2 ≠ 0) : HolonomicCertificate

Build an order-2 certificate with leading p2 ≠ 0.

Equations

• ISAR.orderTwoCert p0 p1 p2 hp2 = { order := 2, coeffs := fun (i : Fin (2 + 1)) => if ↑i = 0 then p0 else if ↑i = 1 then p1 else p2, leading_ne := ⋯ }

theorem ISAR.orderOneCert_residual (p0 p1 : Polynomial ℝ) (hp1 : p1 ≠ 0) (f : ℝ → ℝ) (x : ℝ) : (orderOneCert p0 p1 hp1).residual f x = Polynomial.eval x p0 * f x + Polynomial.eval x p1 * deriv f x

theorem ISAR.orderTwoCert_residual (p0 p1 p2 : Polynomial ℝ) (hp2 : p2 ≠ 0) (f : ℝ → ℝ) (x : ℝ) : (orderTwoCert p0 p1 p2 hp2).residual f x = Polynomial.eval x p0 * f x + Polynomial.eval x p1 * deriv f x + Polynomial.eval x p2 * iteratedDeriv 2 f x

noncomputable def ISAR.HolonomicCertificate.integralShift (c : HolonomicCertificate) : HolonomicCertificate

Prepend a zero coefficient (integral-closure construction).

Equations

• c.integralShift = { order := c.order + 1, coeffs := fun (i : Fin (c.order + 1 + 1)) => if h : ↑i = 0 then 0 else c.coeffs ⟨↑i - 1, ⋯⟩, leading_ne := ⋯ }