The quadratic truncation and Taylor estimate for the exponential

For an algebra A over a field, with A a topological ring, the third partial sum of NormedSpace.expSeries is 1 + x + 2⁻¹ • x ^ 2. This identity needs no norm or completeness assumption. In a complete normed algebra, the exponential agrees with this quadratic truncation to third order at the origin. This file records that estimate in Asymptotics.IsBigO form.

The exponential is analytic at 0 with power series NormedSpace.expSeries, so the statement is the Taylor formula HasFPowerSeriesAt.isBigO_sub_partialSum_pow at n = 3, once the third partial sum of expSeries is evaluated. The quadratic order pins down the second-order term of the Baker--Campbell--Hausdorff expansion.

Main results

• NormedSpace.expSeries_partialSum_three: the third partial sum of the exponential series is 1 + x + 2⁻¹ • x ^ 2.
• NormedSpace.isBigO_exp_sub_quadratic: exp x - (1 + x + 2⁻¹ • x ^ 2) is O(‖x‖ ^ 3) at the origin.

@[simp]

theorem NormedSpace.expSeries_partialSum_three (𝕂 : Type u_1) {A : Type u_2} [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] (x : A) : (expSeries 𝕂 A).partialSum 3 x = 1 + x + 2⁻¹ • x ^ 2

For an algebra A over a field, with A a topological ring, the third partial sum of the exponential series is the quadratic truncation 1 + x + 2⁻¹ • x ^ 2.

theorem NormedSpace.isBigO_exp_sub_quadratic (𝕂 : Type u_1) {A : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [CompleteSpace A] : (fun (x : A) => exp x - (1 + x + 2⁻¹ • x ^ 2)) =O[nhds 0] fun (x : A) => ‖x‖ ^ 3

The quadratic Taylor estimate for the exponential. In a complete normed algebra, exp x - (1 + x + 2⁻¹ • x ^ 2) is O(‖x‖ ^ 3) as x → 0.