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

ParallelTransportPreservesInnerProduct

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)

 100def ParallelTransportPreservesInnerProduct (g : MetricTensor) (γ : SpacetimeCurve) : Prop :=

proof body

Definition body.

 101  ∀ V W : ℝ → (Fin 4 → ℝ),
 102    SmoothField V →
 103    SmoothField W →
 104    ParallelTransported g γ V →
 105    ParallelTransported g γ W →
 106    ∀ lam,
 107      deriv (fun l =>
 108        Finset.univ.sum (fun μ =>
 109          Finset.univ.sum (fun ν =>
 110            g.g (γ.path l) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 111            V l μ * W l ν))) lam = 0
 112
 113/-- For Minkowski, inner product preservation holds: g(V,W) is constant
 114    along any curve when V, W are parallel-transported (both constant in flat space).
 115
 116    The proof uses the fact that η is position-independent and both V, W
 117    have vanishing derivatives (proved by `parallel_transport_flat`).
 118    The derivative of Σ (const * const * const) = 0. -/

used by (2)

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

depends on (29)

Lean names referenced from this declaration's body.