SpacelikeGeodesic

formal source

 136        (deriv (fun lam' => path lam' ν) lam))) = 0
 137
 138/-- A spacelike geodesic: path with positive interval, using real Christoffel. -/
 139structure SpacelikeGeodesic (g : MetricTensor) extends RealGeodesic g where
 140  spacelike_condition : ∀ lam : ℝ,
 141    0 < Finset.sum Finset.univ (fun μ =>
 142      Finset.sum Finset.univ (fun ν =>
 143        g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 144        (deriv (fun lam' => path lam' μ) lam) *
 145        (deriv (fun lam' => path lam' ν) lam)))
 146
 147/-- Proof that `RealGeodesic` uses the real Christoffel symbols from `Curvature.christoffel`,
 148    not the scaffold `Connection.christoffel_from_metric`. -/
 149theorem geodesic_uses_real_christoffel (g : MetricTensor) (geo : RealGeodesic g)
 150    (lam : ℝ) (μ : Fin 4) :
 151    deriv (deriv (fun lam' => geo.path lam' μ)) lam +
 152    Finset.sum Finset.univ (fun ρ =>
 153      Finset.sum Finset.univ (fun σ =>
 154        christoffel g (geo.path lam) μ ρ σ *
 155        (deriv (fun lam' => geo.path lam' ρ) lam) *
 156        (deriv (fun lam' => geo.path lam' σ) lam))) = 0 :=
 157  geo.geodesic_equation lam μ
 158
 159/-- Straight lines are geodesics of Minkowski spacetime (using real Christoffel). -/
 160theorem minkowski_straight_line_geodesic (x₀ v : Fin 4 → ℝ) :
 161    ∃ geo : RealGeodesic minkowski_tensor,
 162      (∀ lam μ, geo.path lam μ = x₀ μ + lam * v μ) := by
 163  refine ⟨{
 164    path := fun lam μ => x₀ μ + lam * v μ
 165    geodesic_equation := ?_
 166  }, ?_⟩
 167  · intro lam μ
 168    simp [minkowski_real_christoffel_zero, Finset.sum_const_zero]
 169  · intro lam μ; rfl