SmoothField

formal source

  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. -/
  85theorem parallel_transport_flat (γ : SpacetimeCurve)
  86    (V : ℝ → (Fin 4 → ℝ))
  87    (h_pt : ParallelTransported minkowski_tensor γ V) :
  88    ∀ lam μ, deriv (fun l => V l μ) lam = 0 := by
  89  intro lam μ
  90  have h := h_pt lam μ
  91  simp only [minkowski_christoffel_zero_proper, zero_mul, Finset.sum_const_zero, add_zero] at h
  92  exact h
  93
  94/-- Parallel transport preserves the metric inner product.
  95    If V, W are parallel-transported along γ, then g(V,W) is constant.