English
The stereoInvFunAux map is smooth of class ContDiff for all smoothness levels; in particular stereoInvFunAux v is continuously differentiable of all orders with respect to its argument.
Русский
Функция stereoInvFunAux v гладкая: она относится к классу ContDiff для всех степеней гладкости; она непрерывно дифференцируема во всех порядках по аргументу.
LaTeX
$$$\\operatorname{ContDiff}_{\\mathbb{R}} m\\; (\\text{stereoInvFunAux } v) \\,(\\text{для любого } m)$$$
Lean4
theorem contDiff_stereoInvFunAux {m : WithTop ℕ∞} : ContDiff ℝ m (stereoInvFunAux v) :=
by
have h₀ : ContDiff ℝ ω fun w : E => ‖w‖ ^ 2 := contDiff_norm_sq ℝ
have h₁ : ContDiff ℝ ω fun w : E => (‖w‖ ^ 2 + 4)⁻¹ :=
by
refine (h₀.add contDiff_const).inv ?_
intro x
nlinarith
have h₂ : ContDiff ℝ ω fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v :=
by
refine (contDiff_const.smul contDiff_id).add ?_
exact (h₀.sub contDiff_const).smul contDiff_const
exact (h₁.smul h₂).of_le le_top
