deriv_coordRay_j

formal source

 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]
 391  exact deriv_const 0 (x j)
 392
 393/-- **THEOREM**: Functional derivative of spatialNormSq.
 394    ∂_μ (∑ x_i²) = 2 x_μ for μ ∈ {1,2,3}, else 0.
 395
 396    **Derivation**: Using the chain rule and ∂_μ(x_i²) = 2x_i δ_{iμ}, we get:
 397    ∂_μ(x₁² + x₂² + x₃²) = 2x₁δ_{1μ} + 2x₂δ_{2μ} + 2x₃δ_{3μ} = 2x_μ for μ ∈ {1,2,3}. -/
 398theorem partialDeriv_v2_spatialNormSq (μ : Fin 4) (x : Fin 4 → ℝ) :
 399    partialDeriv_v2 spatialNormSq μ x =
 400    if μ = 0 then 0 else 2 * x μ := by
 401  -- Each component x_i² gives 2x_i δ_{iμ}
 402  have hd1 := partialDeriv_v2_x_sq μ 1 x
 403  have hd2 := partialDeriv_v2_x_sq μ 2 x
 404  have hd3 := partialDeriv_v2_x_sq μ 3 x
 405  -- Enumerate all 4 cases for μ
 406  fin_cases μ <;> simp_all [partialDeriv_v2, spatialNormSq, coordRay_apply, basisVec, deriv_const_add]
 407
 408/-- Differentiability of spatialNormSq along a coordinate ray. -/
 409theorem differentiableAt_coordRay_spatialNormSq (x : Fin 4 → ℝ) (μ : Fin 4) :
 410    DifferentiableAt ℝ (fun t => spatialNormSq (coordRay x μ t)) 0 := by
 411  unfold spatialNormSq
 412  apply DifferentiableAt.add
 413  · apply DifferentiableAt.add
 414    · exact differentiableAt_coordRay_i_sq x μ 1
 415    · exact differentiableAt_coordRay_i_sq x μ 2
 416  · exact differentiableAt_coordRay_i_sq x μ 3
 417
 418/-- Differentiability of spatialRadius along a coordinate ray. -/