English
The inverse map of the unit ball transformation is C^n on the unit ball, i.e. its inverse is C^n smooth there.
Русский
Обратная карта преобразования единичного шара гладкая класса C^n на единичном шаре.
LaTeX
$$$\\text{ContDiffOn}_{\\mathbb{R}}^{n} (\\mathrm{univUnitBall})^{-1}\\; (\\mathbb{B}(0,1))$$$
Lean4
theorem contDiffOn_univUnitBall_symm : ContDiffOn ℝ n univUnitBall.symm (ball (0 : E) 1) := fun y hy ↦
by
apply ContDiffAt.contDiffWithinAt
suffices ContDiffAt ℝ n (fun y : E => (√(1 - ‖y‖ ^ 2 : ℝ))⁻¹) y from this.smul contDiffAt_id
have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by
rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
refine ContDiffAt.inv ?_ (Real.sqrt_ne_zero'.mpr h)
change ContDiffAt ℝ n ((fun y ↦ √(y)) ∘ fun y ↦ (1 - ‖y‖ ^ 2)) y
refine (contDiffAt_sqrt h.ne').comp y ?_
exact contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt
