Reindexing the literal primary/corrector packet into its actual power coefficients.

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

Shift up as an element of ℕ → V | 0 => 0 | n+1 => truncate M u n.

Equations

• EulerFiniteGrades.shiftUp M u 0 = 0
• EulerFiniteGrades.shiftUp M u n.succ = EulerFiniteGrades.truncate M u n

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

Assemble, given by truncate M u n + shiftUp M c n.

Equations

• EulerFiniteGrades.assemble M u c n = EulerFiniteGrades.truncate M u n + EulerFiniteGrades.shiftUp M c n

theorem EulerFiniteGrades.evaluate_shiftUp {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (u : ℕ → V) : evaluate (M + 1) κ (shiftUp M u) = κ • evaluate M κ u

theorem EulerFiniteGrades.evaluate_assemble {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (u c : ℕ → V) : evaluate (M + 1) κ (assemble M u c) = evaluate M κ u + κ • evaluate M κ c

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

theorem EulerFiniteGrades.evaluate_assemble_from_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (u c : ℕ → V) (hu : u 0 = 0) (hc : c 0 = 0) : evaluate (M + 1) κ (assemble M u c) = ∑ i ∈ Finset.range M, (κ ^ (i + 1) • u (i + 1) + κ ^ (i + 2) • c (i + 1))

Equation (13), with the extra final corrector retained rather than dropped.

theorem EulerFiniteGrades.assemble_zero {V : Type u_1} [AddCommGroup V] (M : ℕ) (u c : ℕ → V) (hu : u 0 = 0) : assemble M u c 0 = 0

theorem EulerFiniteGrades.assemble_interior {V : Type u_1} [AddCommGroup V] (M n : ℕ) (hn : 1 ≤ n) (hMn : n ≤ M) (u c : ℕ → V) : assemble M u c n = u n + c (n - 1)

theorem EulerFiniteGrades.assemble_last {V : Type u_1} [AddCommGroup V] (M : ℕ) (u c : ℕ → V) : assemble M u c (M + 1) = c M

theorem EulerFiniteGrades.assemble_above {V : Type u_1} [AddCommGroup V] (M n : ℕ) (hn : M + 1 < n) (u c : ℕ → V) : assemble M u c n = 0