case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ n f y
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
⊢ ContDiffWithinAt ℝ n f (ball 0 1) y
apply ContDiffAt.contDiffWithinAt
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ ContDiffAt ℝ n f y
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ n f y
have hf : f =ᶠ[𝓝 y] fun y => ((1 : ℝ) - ‖(y : E)‖ ^ 2).sqrt⁻¹ • (y : E) := by
  filter_upwards [isOpen_ball.mem_nhds hy] with z hz
  rw [h z hz]
  rfl
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) y
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ ContDiffAt ℝ n f y
refine' ContDiffAt.congr_of_eventuallyEq _ hf
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) y
suffices ContDiffAt ℝ n (fun y => ((1 : ℝ) - ‖(y : E)‖ ^ 2).sqrt⁻¹) y from this.smul contDiffAt_id
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h✝ : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
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
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h✝ : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => sqrt (1 - ‖y‖ ^ 2)) y
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h✝ : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
refine' ContDiffAt.inv _ (Real.sqrt_ne_zero'.mpr h)
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h✝ : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => 1 - ‖y‖ ^ 2) y
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h✝ : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => sqrt (1 - ‖y‖ ^ 2)) y
refine' (contDiffAt_sqrt h.ne').comp y _
no goals
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h✝ : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => 1 - ‖y‖ ^ 2) y
exact contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
z : E
hz : z ∈ ball 0 1
⊢ f z = (sqrt (1 - ‖z‖ ^ 2))⁻¹ • z
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
⊢ f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
filter_upwards [isOpen_ball.mem_nhds hy] with z hz
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
z : E
hz : z ∈ ball 0 1
⊢ ↑(Homeomorph.symm homeomorphUnitBall) { val := z, property := hz } = (sqrt (1 - ‖z‖ ^ 2))⁻¹ • z
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
z : E
hz : z ∈ ball 0 1
⊢ f z = (sqrt (1 - ‖z‖ ^ 2))⁻¹ • z
rw [h z hz]
no goals
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
z : E
hz : z ∈ ball 0 1
⊢ ↑(Homeomorph.symm homeomorphUnitBall) { val := z, property := hz } = (sqrt (1 - ‖z‖ ^ 2))⁻¹ • z
rfl
no goals
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : E → E
h : ∀ (y : E) (hy : y ∈ ball 0 1), f y = ↑(Homeomorph.symm homeomorphUnitBall) { val := y, property := hy }
y : E
hy : y ∈ ball 0 1
hf : f =ᶠ[𝓝 y] fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹ • y
⊢ 0 < 1 - ‖y‖ ^ 2
rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy