contDiff_univUnitBall — Mathlib

English

The map x ↦ x/√(1+‖x‖^2) from E to E is C^n for any n, hence it is continuously differentiable to all orders.

Русский

Отображение x ↦ x/√(1+∥x∥^2) с E в E принадлежит классу C^n для любого n; то есть оно гладко до любого порядка.

LaTeX

$$$\\text{ContDiff}_{\\mathbb{R}}^{n} \\left(x \\mapsto \\frac{x}{\\sqrt{1+\\|x\\|^2}}\\right)$$$

Lean4

theorem contDiff_univUnitBall : ContDiff ℝ n (univUnitBall : E → E) :=
  by
  suffices ContDiff ℝ n fun x : E => (√(1 + ‖x‖ ^ 2 : ℝ))⁻¹ from this.smul contDiff_id
  have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
  refine ContDiff.inv ?_ fun x => Real.sqrt_ne_zero'.mpr (h x)
  exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'

Похожие утверждения