Physicslib4.Spacetime.AlongPath

Vector fields and covariant derivatives along smooth paths

Two facts make the chart-free geodesic condition (def:geodesic) well defined and non-vacuous:

• SmoothPath.covDeriv_eq_of_eventuallyEq: (∇_{μ'(s)} Y)(μ s) depends only on the values of Y along μ near s;
• SmoothPath.exists_vectorField_eq_tangent: near an interior parameter, the velocity of a smooth path extends to a smooth vector field on the spacetime.

Blueprint reference: lmm:derivative-vanishes-along-path, lmm:covariant-derivative-along-curve-local, lmm:local-vector-field-globalises, lmm:path-local-left-inverse, lmm:velocity-extends.

theorem Physicslib4.Spacetime.SmoothPath.mfderiv_apply_tangent_eq_zero {M : Spacetime} (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) {f : M.Carrier → ℝ} (hf : MDiffAt f (μ.toFun s)) (h0 : ∀ᶠ (t : ℝ) in nhdsWithin s μ.parameterSpace, f (μ.toFun t) = 0) : (have this := (mfderiv% f (μ.toFun s)) (μ.tangent s); this) = 0

A function vanishing along a path has zero derivative along it. If f is differentiable at μ s and f ∘ μ vanishes on the parameter space near s, then df(μ'(s)) = 0.

Blueprint reference: lmm:derivative-vanishes-along-path.

theorem Physicslib4.Spacetime.SmoothPath.covDeriv_eq_of_eventuallyEq {M : Spacetime} (cov : CovariantDerivative M.model SpacetimeModel (TangentSpace M.model)) (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) {Y Y' : (x : M.Carrier) → TangentSpace M.model x} (hY : (MDiffAt fun (x : M.Carrier) => ⟨x, Y x⟩) (μ.toFun s)) (hY' : (MDiffAt fun (x : M.Carrier) => ⟨x, Y' x⟩) (μ.toFun s)) (h : ∀ᶠ (t : ℝ) in nhdsWithin s μ.parameterSpace, Y (μ.toFun t) = Y' (μ.toFun t)) : (↑cov Y (μ.toFun s)) (μ.tangent s) = (↑cov Y' (μ.toFun s)) (μ.tangent s)

The covariant derivative along a path is local. For a covariant derivative ∇ on the tangent bundle, (∇_{μ'(s)} Y)(μ s) depends only on the values of Y along μ near s.

Blueprint reference: lmm:covariant-derivative-along-curve-local.

theorem Physicslib4.Spacetime.exists_contMDiff_vectorField_eventuallyEq {M : Spacetime} {p : M.Carrier} {U : Set M.Carrier} (hU : IsOpen U) (hp : p ∈ U) {X₀ : (x : M.Carrier) → TangentSpace M.model x} (hX₀ : ContMDiffOn M.model (M.model.prod (modelWithCornersSelf ℝ SpacetimeModel)) (↑⊤) (fun (x : M.Carrier) => ⟨x, X₀ x⟩) U) : ∃ (X : (x : M.Carrier) → TangentSpace M.model x), (ContMDiff M.model (M.model.prod (modelWithCornersSelf ℝ SpacetimeModel)) ↑⊤ fun (x : M.Carrier) => ⟨x, X x⟩) ∧ X =ᶠ[nhds p] X₀

Local vector fields globalise. A vector field smooth on an open neighbourhood of p agrees near p with a smooth vector field on the whole spacetime.

Blueprint reference: lmm:local-vector-field-globalises.

theorem Physicslib4.Spacetime.SmoothPath.exists_localLeftInverse {M : Spacetime} (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ interior μ.parameterSpace) : ∃ (τ : M.Carrier → ℝ), (∀ᶠ (y : M.Carrier) in nhds (μ.toFun s), ContMDiffAt M.model (modelWithCornersSelf ℝ ℝ) (↑⊤) τ y) ∧ ∀ᶠ (t : ℝ) in nhds s, τ (μ.toFun t) = t

Local left inverse of a smooth path. Near an interior parameter s, there is a function τ, smooth near μ s, with τ (μ t) = t for t near s.

Blueprint reference: lmm:path-local-left-inverse.

theorem Physicslib4.Spacetime.SmoothPath.exists_vectorField_eq_tangent {M : Spacetime} (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ interior μ.parameterSpace) : ∃ (X : (x : M.Carrier) → TangentSpace M.model x), (ContMDiff M.model (M.model.prod (modelWithCornersSelf ℝ SpacetimeModel)) ↑⊤ fun (x : M.Carrier) => ⟨x, X x⟩) ∧ ∀ᶠ (t : ℝ) in nhds s, X (μ.toFun t) = μ.tangent t

The velocity of a smooth path extends to a vector field. Near an interior parameter s, there is a smooth vector field X on the spacetime with X (μ t) = μ'(t) for t near s.

Blueprint reference: lmm:velocity-extends.