Factorial Taylor error for bounded observations
Abstract
Factorial Taylor error for bounded observations
Theorem 1.1 (Pointwise Taylor error).
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/ExactTaylorObservationRemainder.norm_observation_taylor_remainder (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let V be a nonzero complete normed space and W a normed space over the real or complex field. Let B:V→V and C:V→W be bounded linear maps, N a natural number, t≥0 and x∈V. No dimension restriction is imposed.
Write b(B)=max(1,‖B‖), c(C)=‖C‖, and p(B,C,N,t,x)=the sum of t^k C(B^k x)/k! for 0≤k≤N. The exponential is the norm-convergent Banach algebra exponential.
The factorial convolution inequality n! k!≤(n+k)! bounds the exponential series tail by r^n exp(r)/n! whenever ‖z‖≤r. Applying C and evaluating at x gives the displayed estimate without a radius restriction.
Theorem 1.2 (Integrated squared Taylor error).
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/ExactTaylorObservationRemainder.observation_taylor_energy_remainder (✓ std3). ∎
Source. Repository-derived.
Commentary.
Under the same hypotheses, let T≥0. The squared norm is integrated with respect to ordinary Lebesgue measure on [0,T]. The result also holds at T=0.
On this interval exp(bt)≤exp(bT). Squaring the pointwise estimate and integrating t^(2N+2) gives exactly the denominator 2N+3. Completeness is needed only for the state-space exponential, not for the scalar energy integral.