Classical division theorem for rational-coefficient E-functions
ProvedArithmeticE.rational_e_function_divisionLet have rational normalized coefficients satisfying the E-function exponential size and common-denominator bounds. Suppose and is annihilated by a nonzero rational polynomial differential operator , with .
There exists a formal series such that , the factorial-normalized coefficients of satisfy the same rational arithmetic conditions, and is annihilated by a rational polynomial differential operator of order with nonzero leading coefficient. Thus division by at the zero preserves the rational-coefficient E-function conditions.
The transformed coefficients are for , and . The value-zero hypothesis is expressed as a convergent real series identity, which is appropriate for rational coefficients at . No arithmetic regularity or value-lifting theorem is assumed.
import Definitions.Def_rationalEArithmetic open ArithmeticE PowerSeries
theorem ArithmeticE.rational_e_function_division (a : ℕ → ℚ) (ha : RationalArithmetic a)
(hz : HasSum (fun n : ℕ => (a n:ℝ)/(n.factorial:ℝ)) 0)
(p : ℕ → Polynomial ℚ) (m : ℕ) (hp : p m ≠ 0)
(hode : ∑ k ∈ Finset.range (m+1), ((p k).map (algebraMap ℚ ℂ):PowerSeries ℂ)*
(PowerSeries.derivative ℂ)^[k] (PowerSeries.mk (fun n => (a n:ℂ)/(n.factorial:ℂ)))=0) :
∃ g : PowerSeries ℂ, RationalSeriesArithmetic g ∧
(1-PowerSeries.X)*g=PowerSeries.mk (fun n => (a n:ℂ)/(n.factorial:ℂ)) ∧
∃ q : ℕ → Polynomial ℚ, q m ≠ 0 ∧
∑ k ∈ Finset.range (m+1), ((q k).map (algebraMap ℚ ℂ):PowerSeries ℂ)*
(PowerSeries.derivative ℂ)^[k] g=0 := by sorry