NullGeodesic

formal source

  17open Calculus
  18
  19/-- Null geodesic: path with zero interval (using lam for affine parameter). -/
  20structure NullGeodesic (g : MetricTensor) where
  21  path : ℝ → (Fin 4 → ℝ)
  22  null_condition : ∀ lam : ℝ,
  23    Finset.sum (Finset.univ : Finset (Fin 4)) (fun μ =>
  24      Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
  25        g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
  26        (deriv (fun lam' => path lam' μ) lam) *
  27        (deriv (fun lam' => path lam' ν) lam))) = 0
  28  geodesic_equation : ∀ lam μ,
  29    deriv (deriv (fun lam' => path lam' μ)) lam +
  30    Finset.sum (Finset.univ : Finset (Fin 4)) (fun ρ =>
  31      Finset.sum (Finset.univ : Finset (Fin 4)) (fun σ =>
  32        (christoffel_from_metric g).Γ (path lam) μ ρ σ *
  33        (deriv (fun lam' => path lam' ρ) lam) *
  34        (deriv (fun lam' => path lam' σ) lam))) = 0
  35
  36/-- Initial conditions for null geodesic. -/
  37structure InitialConditions where
  38  position : Fin 4 → ℝ  -- x^μ(0)
  39  direction : Fin 4 → ℝ  -- k^μ = dx^μ/dλ|_{λ=0}
  40  -- Null condition will be enforced by geodesic structure
  41
  42@[simp] def straight_line (ic : InitialConditions) : ℝ → (Fin 4 → ℝ) :=
  43  fun lam μ => ic.position μ + lam * ic.direction μ
  44
  45/-- Straight coordinate line in Minkowski coordinates. -/
  46def straight_null_geodesic (ic : InitialConditions) : NullGeodesic minkowski_tensor where
  47  path := straight_line ic
  48  null_condition := by
  49    intro lam
  50    classical