radialInv

formal source

 343
 344/-- Radial inverse function `1/r^n` where r is the spatial radius.
 345    Used for gravitational potentials. -/
 346noncomputable def radialInv (n : ℕ) (x : Fin 4 → ℝ) : ℝ :=
 347  1 / (spatialRadius x) ^ n
 348
 349/-- Differentiability of a coordinate ray component. -/
 350theorem differentiableAt_coordRay_i (x : Fin 4 → ℝ) (μ i : Fin 4) :
 351    DifferentiableAt ℝ (fun t => (coordRay x μ t) i) 0 := by
 352  simp only [coordRay_apply]
 353  apply DifferentiableAt.add
 354  · apply differentiableAt_const
 355  · apply DifferentiableAt.mul
 356    · apply differentiableAt_id
 357    · apply differentiableAt_const
 358
 359/-- Differentiability of a squared coordinate ray component. -/
 360theorem differentiableAt_coordRay_i_sq (x : Fin 4 → ℝ) (μ i : Fin 4) :
 361    DifferentiableAt ℝ (fun t => (coordRay x μ t) i ^ 2) 0 := by
 362  apply DifferentiableAt.pow (differentiableAt_coordRay_i x μ i) 2
 363
 364/-- Closed form for ∂μ (xᵢ²). -/
 365theorem partialDeriv_v2_x_sq (μ i : Fin 4) (x : Fin 4 → ℝ) :
 366    partialDeriv_v2 (fun y => y i ^ 2) μ x = 2 * x i * (if i = μ then 1 else 0) := by
 367  unfold partialDeriv_v2
 368  simp only [coordRay_apply]
 369  let f_i := fun t => x i + t * basisVec μ i
 370  have h_f : DifferentiableAt ℝ f_i 0 := differentiableAt_coordRay_i x μ i
 371  rw [show (fun t => (x i + t * basisVec μ i) ^ 2) = f_i ^ 2 by rfl]
 372  rw [deriv_pow h_f 2]
 373  simp only [f_i]
 374  split_ifs with h_eq
 375  · subst h_eq
 376    simp only [basisVec_self, mul_one]