English
For ContDiffOn functions f, the nth derivative of the composition x ↦ f (c x) within s is c^n times the nth derivative of f at c x, under suitable map conditions.
Русский
Для функция на контрольном области ContDiffOn n-ая производная композиции x ↦ f (c x) внутри s равна c^n умножить на n-ую производную f в точке c x, при подходящих условиях отображения.
LaTeX
$$$\\operatorname{iteratedDerivWithin}_n (\\lambda x. f (c x)) s x = c^n \\cdot \\operatorname{iteratedDerivWithin}_n f s (c x)$$$
Lean4
theorem iteratedDerivWithin_comp_const_smul (hf : ContDiffOn 𝕜 n f s) (c : 𝕜) (hs : Set.MapsTo (c * ·) s s) :
iteratedDerivWithin n (fun x => f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x) := by
induction n generalizing x with
| zero => simp
| succ n ih =>
have hcx : c * x ∈ s := hs hx
have h₀ :
s.EqOn (iteratedDerivWithin n (fun x ↦ f (c * x)) s) (fun x => c ^ n • iteratedDerivWithin n f s (c * x)) :=
fun x hx => ih hx hf.of_succ
have h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x) :=
hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx
have h₂ : DifferentiableWithinAt 𝕜 (fun x => iteratedDerivWithin n f s (c * x)) s x :=
by
rw [← Function.comp_def]
apply DifferentiableWithinAt.comp
· exact hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx
· exact differentiableWithinAt_id'.const_mul _
· exact hs
rw [iteratedDerivWithin_succ, derivWithin_congr h₀ (ih hx hf.of_succ), derivWithin_fun_const_smul (c ^ n) h₂,
iteratedDerivWithin_succ, ← Function.comp_def, derivWithin.scomp x h₁ (differentiableWithinAt_id'.const_mul _) hs,
derivWithin_const_mul _ differentiableWithinAt_id', derivWithin_id' _ _ (h _ hx), smul_smul, mul_one, pow_succ]
