differentiableAt_coordRay_i_sq

formal source

 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]
 377    rw [deriv_const_add, deriv_id'']
 378    ring
 379  · simp only [basisVec_ne h_eq, mul_zero, add_zero]
 380    rw [deriv_const]
 381    ring
 382
 383theorem deriv_coordRay_i (x : Fin 4 → ℝ) (i : Fin 4) :
 384    deriv (fun t => (coordRay x i t) i) 0 = 1 := by
 385  simp only [coordRay_apply, basisVec_self, mul_one]
 386  rw [deriv_const_add, deriv_id'']
 387
 388theorem deriv_coordRay_j (x : Fin 4 → ℝ) (i j : Fin 4) (h : j ≠ i) :
 389    deriv (fun t => (coordRay x i t) j) 0 = 0 := by
 390  simp only [coordRay_apply, basisVec_ne h, mul_zero, add_zero]