def
definition
ParallelTransported
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Geometry.ParallelTransport on GitHub at line 54.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
christoffel -
of -
V -
of -
MetricTensor -
of -
of -
V -
MetricTensor -
of -
MetricTensor -
christoffel -
MetricTensor -
SpacetimeCurve -
V
used by
formal source
51 DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0.
52
53 This is the defining ODE for parallel transport. -/
54def ParallelTransported (g : MetricTensor) (γ : SpacetimeCurve)
55 (V : ℝ → (Fin 4 → ℝ)) : Prop :=
56 ∀ lam μ,
57 deriv (fun l => V l μ) lam +
58 Finset.univ.sum (fun α =>
59 Finset.univ.sum (fun β =>
60 christoffel g (γ.path lam) μ α β *
61 γ.tangent lam α *
62 V lam β)) = 0
63
64/-- Smoothness of a vector field along the affine parameter. -/
65def SmoothField (V : ℝ → (Fin 4 → ℝ)) : Prop :=
66 ∀ μ, Differentiable ℝ (fun l => V l μ)
67
68/-- Initial conditions for parallel transport: a vector at parameter λ₀. -/
69structure ParallelTransportIC where
70 lam0 : ℝ
71 V0 : Fin 4 → ℝ
72
73/-- A parallel-transported vector field satisfying initial conditions. -/
74structure ParallelTransportSolution (g : MetricTensor) (γ : SpacetimeCurve)
75 (ic : ParallelTransportIC) where
76 V : ℝ → (Fin 4 → ℝ)
77 is_parallel : ParallelTransported g γ V
78 initial_condition : V ic.lam0 = ic.V0
79
80/-! ## §3 Properties of Parallel Transport -/
81
82/-- In flat Minkowski spacetime, parallel transport is trivial:
83 the Christoffel symbols vanish, so DV/dλ = dV/dλ = 0,
84 meaning V is constant along any curve. -/