English
For a nonzero c, HasFDerivWithinAt (f ∘ (c • ·)) is equivalent to HasFDerivWithinAt (c • f) with adjusted domain and base point.
Русский
Для ненулевого c равенство HasFDerivWithinAt (f ∘ (c • ·)) и HasFDerivWithinAt (c • f) с поправкой области и базовой точки.
LaTeX
$$$$ HasFDerivWithinAt (f \\circ (c \\cdot \\cdot)) f' s x \\iff HasFDerivWithinAt (c \\cdot f) f' (c \\cdot s) (c \\cdot x) $$$$
Lean4
theorem hasFDerivWithinAt_comp_smul_smul_iff {c : 𝕜} :
HasFDerivWithinAt (f <| c • ·) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x) :=
by
rcases eq_or_ne c 0 with rfl | hc
· simp [hasFDerivWithinAt_const, HasFDerivWithinAt.of_subsingleton (subsingleton_zero_smul_set _)]
· lift c to 𝕜ˣ using IsUnit.mk0 c hc
have A : f'.comp ((ContinuousLinearEquiv.smulLeft c : E ≃L[𝕜] E) : E →L[𝕜] E) = c • f' := by ext; simp
rw [← Units.smul_def c x, ← ContinuousLinearEquiv.smulLeft_apply_apply (R₁ := 𝕜), ←
ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, A]
simp [Function.comp_def, ← Units.smul_def, ← preimage_smul_inv, preimage_preimage]
