English
Shifting the input by a constant on the left commutes with taking the iterated derivative within: iteratedFDerivWithin 𝕜 n (f(a+·)) s = x ↦ iteratedFDerivWithin 𝕜 n f (a+ᵥ s) (a+x).
Русский
Сдвиг аргумента слева константой находит взаимно устойчивое свойство с последовательной дифференциацией: iteratedFDerivWithin 𝕜 n (f(a+·)) s = x ↦ iteratedFDerivWithin 𝕜 n f (a+ᵥ s) (a+x).
LaTeX
$$$\forall n\ a\ x,\ iteratedFDerivWithin 𝕜 n (\lambda z, f(a+z)) s = (\lambda x, iteratedFDerivWithin 𝕜 n f (a+ᵥ s) (a+x))$$$
Lean4
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
theorem iteratedFDerivWithin_comp_add_left' (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x) := by
induction n with
| zero => simp [iteratedFDerivWithin]
| succ n IH =>
ext v
rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
simp only [Nat.succ_eq_add_one, IH, comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply]
congr 2
rw [fderivWithin_comp_add_left]
