`differentiableAt_coordRay_spatialNormSq`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Calculus.Derivatives
domain: Relativity
line: 409 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Calculus.Derivatives on GitHub at line 409.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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) :
 429    DifferentiableAt ℝ (fun t => radialInv n (coordRay x μ t)) 0 := by
 430  unfold radialInv
 431  apply DifferentiableAt.div (differentiableAt_const (1 : ℝ))
 432  · apply DifferentiableAt.pow (differentiableAt_coordRay_spatialRadius x μ hx)
 433  · have h_pos : 0 < spatialRadius x := by
 434      unfold spatialRadius
 435      apply Real.sqrt_pos.mpr
 436      have h_nonneg := spatialNormSq_nonneg x
 437      have h_ne_zero := (spatialRadius_ne_zero_iff x).mp hx
 438      exact lt_of_le_of_ne h_nonneg h_ne_zero.symm
 439    simp only [coordRay_zero]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.