theorem
proved
partialDeriv_v2_spatialNormSq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.Calculus.Derivatives on GitHub at line 398.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
all -
of -
all -
of -
partialDeriv_v2 -
of -
of -
for -
of -
all -
basisVec -
coordRay_apply -
partialDeriv_v2 -
partialDeriv_v2_x_sq -
spatialNormSq
used by
formal source
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. -/
419theorem differentiableAt_coordRay_spatialRadius (x : Fin 4 → ℝ) (μ : Fin 4) (hx : spatialRadius x ≠ 0) :
420 DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 := by
421 unfold spatialRadius
422 have h_sn_ne_zero : spatialNormSq (coordRay x μ 0) ≠ 0 := by
423 simp only [coordRay_zero]
424 exact (spatialRadius_ne_zero_iff x).mp hx
425 apply DifferentiableAt.sqrt (differentiableAt_coordRay_spatialNormSq x μ) h_sn_ne_zero
426
427/-- Differentiability of radialInv along a coordinate ray. -/
428theorem differentiableAt_coordRay_radialInv (n : ℕ) (x : Fin 4 → ℝ) (μ : Fin 4) (hx : spatialRadius x ≠ 0) :