pith. machine review for the scientific record. sign in
theorem proved tactic proof

differentiableAt_coordRay_radialInv

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 428theorem differentiableAt_coordRay_radialInv (n : ℕ) (x : Fin 4 → ℝ) (μ : Fin 4) (hx : spatialRadius x ≠ 0) :
 429    DifferentiableAt ℝ (fun t => radialInv n (coordRay x μ t)) 0 := by

proof body

Tactic-mode proof.

 430  unfold radialInv
 431  apply DifferentiableAt.div (differentiableAt_const (1 : ℝ))
 432  · apply DifferentiableAt.pow (differentiableAt_coordRay_spatialRadius x μ hx)
 433  · have h_pos : 0 < spatialRadius x := by
 434      unfold spatialRadius
 435      apply Real.sqrt_pos.mpr
 436      have h_nonneg := spatialNormSq_nonneg x
 437      have h_ne_zero := (spatialRadius_ne_zero_iff x).mp hx
 438      exact lt_of_le_of_ne h_nonneg h_ne_zero.symm
 439    simp only [coordRay_zero]
 440    exact (pow_pos h_pos n).ne'
 441

depends on (10)

Lean names referenced from this declaration's body.