pith. machine review for the scientific record. sign in
structure definition def or abbrev

ParallelTransportSolution

show as:
view Lean formalization →

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)

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.