398theorem partialDeriv_v2_spatialNormSq (μ : Fin 4) (x : Fin 4 → ℝ) : 399 partialDeriv_v2 spatialNormSq μ x = 400 if μ = 0 then 0 else 2 * x μ := by
proof body
Term-mode proof.
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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.