No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
419theorem differentiableAt_coordRay_spatialRadius (x : Fin 4 → ℝ) (μ : Fin 4) (hx : spatialRadius x ≠ 0) :
420 DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 := by
proof body
Tactic-mode proof.
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. -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
coordRay
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
coordRay_zero
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
differentiableAt_coordRay_spatialNormSq
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
radialInv
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
spatialNormSq
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
spatialRadius
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
spatialRadius_ne_zero_iff
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use