Finite Taylor reconstruction

Application-independent finite Taylor reconstruction for a nilpotent endomorphism. Extracted from Stafford38 commit c8a513d553b24c7c08da82f496c44dbbaeb1f2fc.

def AlgebraicAnalysis.FiniteTaylorReconstruction.projectorMapG {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (K : ℕ) (S D : V →ₗ[𝕜] V) : V →ₗ[𝕜] V

The finite alternating Taylor projector associated with two endomorphisms.

Equations

• AlgebraicAnalysis.FiniteTaylorReconstruction.projectorMapG K S D = ∑ r ∈ Finset.range (K + 1), ((-1) ^ r / ↑r.factorial) • (S ^ r * D ^ r)

theorem AlgebraicAnalysis.FiniteTaylorReconstruction.reconstruction_all {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (K : ℕ) (S D : V →ₗ[𝕜] V) (x : V) (hnil : (D ^ (K + 1)) x = 0) : x = ∑ j ∈ Finset.range (K + 1), (1 / ↑j.factorial) • (S ^ j * projectorMapG K S D * D ^ j) x

The all-order finite Taylor reconstruction for a nilpotent derivative.

The following wrapper turns the endomorphism statement into the concrete algebraic form used in a Weyl chart. It deliberately stops at the abstract ring/module interface: the A₂-specific work of constructing s, proving D s = 1, and proving nilpotence on the chosen element remains external.