Degree bounds and the exact shift caused by a fast derivative.

@[simp]

theorem EulerFiniteGrades.truncate_of_le {V : Type u_1} [AddCommGroup V] (M n : ℕ) (u : ℕ → V) (hn : n ≤ M) : truncate M u n = u n

@[simp]

theorem EulerFiniteGrades.truncate_of_gt {V : Type u_1} [AddCommGroup V] (M n : ℕ) (u : ℕ → V) (hn : M < n) : truncate M u n = 0

theorem EulerFiniteGrades.evaluate_extend {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M N : ℕ) (hMN : M ≤ N) (κ : ℝ) (u : ℕ → V) (hu : ∀ (n : ℕ), M < n → u n = 0) : evaluate N κ u = evaluate M κ u

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

theorem EulerFiniteGrades.evaluate_truncate_extend {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M N : ℕ) (hMN : M ≤ N) (κ : ℝ) (u : ℕ → V) : evaluate N κ (truncate M u) = evaluate M κ u

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

Shift down, given by truncate M u (n+1).

Equations

• EulerFiniteGrades.shiftDown M u n = EulerFiniteGrades.truncate M u (n + 1)

theorem EulerFiniteGrades.shiftDown_above {V : Type u_1} [AddCommGroup V] (M n : ℕ) (u : ℕ → V) (hn : M ≤ n) : shiftDown M u n = 0

theorem EulerFiniteGrades.inverse_evaluate_shiftDown {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (u : ℕ → V) (hu : u 0 = 0) : κ⁻¹ • evaluate M κ u = evaluate M κ (shiftDown M u)

theorem EulerFiniteGrades.inverse_evaluate_shiftDown_extend {V : Type u_1} [AddCommGroup V] [Module ℝ V] (M N : ℕ) (hMN : M ≤ N) (κ : ℝ) (hκ : κ ≠ 0) (u : ℕ → V) (hu : u 0 = 0) : κ⁻¹ • evaluate M κ u = evaluate N κ (shiftDown M u)