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)
409theorem differentiableAt_coordRay_spatialNormSq (x : Fin 4 → ℝ) (μ : Fin 4) :
410 DifferentiableAt ℝ (fun t => spatialNormSq (coordRay x μ t)) 0 := by
proof body
Term-mode proof.
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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
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
-
differentiableAt_coordRay_i_sq
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
spatialNormSq
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
spatialRadius
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use