English
Symmetric recursion on the right: iteratedPDeriv 𝕜 m f equals pderivCLM 𝕜 (m (Fin.last n)) applied to iteratedPDeriv 𝕜 (Fin.init m) f.
Русский
Симметричная рекурсия справа: iteratedPDeriv 𝕜 m f = pderivCLM 𝕜 (m (Fin.last n)) (iteratedPDeriv 𝕜 (Fin.init m) f).
LaTeX
$$$iteratedPDeriv 𝕜\, m\, f = pderivCLM 𝕜 (m (Fin.last n)) (iteratedPDeriv 𝕜 (Fin.init m) f)$$$
Lean4
theorem iteratedPDeriv_succ_right {n : ℕ} (m : Fin (n + 1) → E) (f : 𝓢(E, F)) :
iteratedPDeriv 𝕜 m f = iteratedPDeriv 𝕜 (Fin.init m) (pderivCLM 𝕜 (m (Fin.last n)) f) := by
induction n with
| zero =>
rw [iteratedPDeriv_zero, iteratedPDeriv_one, Fin.last_zero]
-- The proof is `∂^{n + 2} = ∂ ∂^{n + 1} = ∂ ∂^n ∂ = ∂^{n+1} ∂`
| succ n IH =>
have hmzero : Fin.init m 0 = m 0 := by simp only [Fin.init_def, Fin.castSucc_zero]
have hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ) := by simp only [Fin.tail_def, Fin.succ_last]
calc
_ = pderivCLM 𝕜 (m 0) (iteratedPDeriv 𝕜 _ f) := iteratedPDeriv_succ_left _ _ _
_ = pderivCLM 𝕜 (m 0) ((iteratedPDeriv 𝕜 _) ((pderivCLM 𝕜 _) f)) :=
by
congr 1
exact IH _
_ = _ := by simp only [hmtail, iteratedPDeriv_succ_left, hmzero, Fin.tail_init_eq_init_tail]
