ParallelTransportPreservesInnerProduct

formal source

  97    g_{μν} V^μ W^ν = const along γ
  98
  99    This is a consequence of metric compatibility ∇g = 0. -/
 100def ParallelTransportPreservesInnerProduct (g : MetricTensor) (γ : SpacetimeCurve) : Prop :=
 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. -/
 119theorem minkowski_preserves_inner (γ : SpacetimeCurve) :
 120    ParallelTransportPreservesInnerProduct minkowski_tensor γ := by
 121  intro V W h_diffV h_diffW hV hW lam
 122  have hV_const := parallel_transport_flat γ V hV
 123  have hW_const := parallel_transport_flat γ W hW
 124  let t0 : ℝ → ℝ := fun l => V l 0 * W l 0
 125  let t1 : ℝ → ℝ := fun l => V l 1 * W l 1
 126  let t2 : ℝ → ℝ := fun l => V l 2 * W l 2
 127  let t3 : ℝ → ℝ := fun l => V l 3 * W l 3
 128  have ht0_diff : DifferentiableAt ℝ t0 lam := by
 129    unfold t0
 130    exact (h_diffV 0 lam).mul (h_diffW 0 lam)