Translating C^n functions on balls #
Translating the argument of a function f by a moves the ball on which f is C^n:
if f is C^n on ball x R, then y ↦ f (y + a) is C^n on ball (x - a) R. The case
a = x recentres a ball computation at the origin.
Main declarations #
ContDiffOn.comp_add_right_ball: translation of aC^nfunction on a ball.
theorem
ContDiffOn.comp_add_right_ball
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{f : E → F}
{x : E}
{R : ℝ}
(hf : ContDiffOn 𝕜 n f (Metric.ball x R))
(a : E)
:
ContDiffOn 𝕜 n (fun (y : E) => f (y + a)) (Metric.ball (x - a) R)
If f is C^n on the ball ball x R, then its translate y ↦ f (y + a) is C^n on the
translated ball ball (x - a) R.