Exact finite graded identities for the literal packet residual.

def EulerFiniteGrades.evaluate {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (u : ℕ → V) : V

Evaluate, given by ∑ n ∈ range (M+1), κ^n • u n.

Equations

• EulerFiniteGrades.evaluate M κ u = ∑ n ∈ Finset.range (M + 1), κ ^ n • u n

def EulerFiniteGrades.truncate {V : Type u_1} [AddCommGroup V] (M : ℕ) (u : ℕ → V) (n : ℕ) : V

Truncate, with branches according to n ≤ M.

Equations

• EulerFiniteGrades.truncate M u n = if n ≤ M then u n else 0

def EulerFiniteGrades.convolution {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M : ℕ) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u : ℕ → V) (v : ℕ → W) (n : ℕ) : Q

Convolution, given by ∑ i ∈ range (M+1), ∑ j ∈ range (M+1), if i+j=n then B (u i) (v j) else 0.

Equations

• EulerFiniteGrades.convolution M B u v n = ∑ i ∈ Finset.range (M + 1), ∑ j ∈ Finset.range (M + 1), if i + j = n then (B (u i)) (v j) else 0

theorem EulerFiniteGrades.evaluate_add {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (u v : ℕ → V) : (evaluate M κ fun (n : ℕ) => u n + v n) = evaluate M κ u + evaluate M κ v

theorem EulerFiniteGrades.map_evaluate {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (M : ℕ) (κ : ℝ) (L : V →ₗ[ℝ] W) (u : ℕ → V) : L (evaluate M κ u) = evaluate M κ fun (n : ℕ) => L (u n)

theorem EulerFiniteGrades.bilinear_evaluate {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M : ℕ) (κ : ℝ) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u : ℕ → V) (v : ℕ → W) : (B (evaluate M κ u)) (evaluate M κ v) = evaluate (2 * M) κ (convolution M B u v)

Bilinearity expands the actual finite evaluated packet into its exact grades.

theorem EulerFiniteGrades.convolution_above {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M n : ℕ) (hn : 2 * M < n) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u : ℕ → V) (v : ℕ → W) : convolution M B u v n = 0

theorem EulerFiniteGrades.convolution_zero {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M : ℕ) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u : ℕ → V) (v : ℕ → W) (hu : u 0 = 0) : convolution M B u v 0 = 0

theorem EulerFiniteGrades.inverse_evaluate {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (u : ℕ → V) (hu : u 0 = 0) : κ⁻¹ • evaluate M κ u = ∑ n ∈ Finset.range M, κ ^ n • u (n + 1)

A vanishing constant term justifies the fast derivative's inverse power of κ.

theorem EulerFiniteGrades.evaluate_eq_tail {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M K : ℕ) (hK : K ≤ M + 1) (κ : ℝ) (u : ℕ → V) (hzero : ∀ n < K, u n = 0) : evaluate M κ u = ∑ n ∈ Finset.Ico K (M + 1), κ ^ n • u n

Exact cancellation of low grades leaves only the literal finite high-grade tail.