Holonomic closure theorems

Python counterparts:

• HolonomicRegistry.integral_closure — coefficient shift theorem
• product_closure — order-1 multiplicative product (tensor bound 1)
• sum_closure — constant-rate order-1 sum (order ≤ 2)

theorem ISAR.iteratedDeriv_of_deriv_eq {g h : ℝ → ℝ} (hg : deriv h = g) (n : ℕ) : iteratedDeriv (n + 1) h = iteratedDeriv n g

If deriv h = g as functions, higher derivatives of h match those of g shifted.

theorem ISAR.integral_closure_shift (c : HolonomicCertificate) (g h : ℝ → ℝ) (hg : satisfiesODE c g) (hd : deriv h = g) : satisfiesODE c.integralShift h

Integral closure shift (Python integral_closure).

def ISAR.satisfiesOrderOneMultiplicative (a : Polynomial ℝ) (f : ℝ → ℝ) : Prop

Order-1 multiplicative form: f' = a · f with polynomial a.

Equations

• ISAR.satisfiesOrderOneMultiplicative a f = ∀ (x : ℝ), deriv f x = Polynomial.eval x a * f x

theorem ISAR.satisfiesOrderOneMultiplicative.to_satisfiesODE (a : Polynomial ℝ) (f : ℝ → ℝ) (hf : satisfiesOrderOneMultiplicative a f) : satisfiesODE (orderOneCert (-a) 1 ⋯) f

theorem ISAR.product_orderOne_multiplicative (a b : Polynomial ℝ) (f g : ℝ → ℝ) (hf : satisfiesOrderOneMultiplicative a f) (hg : satisfiesOrderOneMultiplicative b g) (hdf : Differentiable ℝ f) (hdg : Differentiable ℝ g) : satisfiesOrderOneMultiplicative (a + b) (f * g)

Product of two order-1 multiplicative holonomic functions is again order-1 multiplicative.

theorem ISAR.product_holonomic_orderOne (a b : Polynomial ℝ) (f g : ℝ → ℝ) (hf : satisfiesOrderOneMultiplicative a f) (hg : satisfiesOrderOneMultiplicative b g) (hdf : Differentiable ℝ f) (hdg : Differentiable ℝ g) : satisfiesODE (orderOneCert (-(a + b)) 1 ⋯) (f * g)

Product closure for order-1 multiplicative certificates (order bound ≤ 1·1 = 1).

theorem ISAR.sum_holonomic_const_rates (a b : ℝ) (f g : ℝ → ℝ) (hf : satisfiesOrderOneMultiplicative (Polynomial.C a) f) (hg : satisfiesOrderOneMultiplicative (Polynomial.C b) g) (hdf : Differentiable ℝ f) (hdg : Differentiable ℝ g) : satisfiesODE (orderTwoCert (Polynomial.C (a * b)) (Polynomial.C (-(a + b))) 1 ⋯) (f + g)

Sum closure for constant-rate order-1 factors (a, b ∈ ℝ), order bound ≤ 2.

theorem ISAR.product_holonomic_orderOne_exists (a b : Polynomial ℝ) (f g : ℝ → ℝ) (hf : satisfiesOrderOneMultiplicative a f) (hg : satisfiesOrderOneMultiplicative b g) (hdf : Differentiable ℝ f) (hdg : Differentiable ℝ g) : IsHolonomic (f * g)

theorem ISAR.sum_holonomic_const_rates_exists (a b : ℝ) (f g : ℝ → ℝ) (hf : satisfiesOrderOneMultiplicative (Polynomial.C a) f) (hg : satisfiesOrderOneMultiplicative (Polynomial.C b) g) (hdf : Differentiable ℝ f) (hdg : Differentiable ℝ g) : IsHolonomic (f + g)