null_geodesic_exists_minkowski

formal source

  65    simp [straight_line, deriv_const_mul, christoffel_from_metric, partialDeriv]
  66
  67/-- Existence of a straight null geodesic for Minkowski background. -/
  68theorem null_geodesic_exists_minkowski (ic : InitialConditions) :
  69    ∃ geo : NullGeodesic minkowski_tensor,
  70      geo.path 0 = ic.position ∧
  71      (∀ μ, deriv (fun lam => geo.path lam μ) 0 = ic.direction μ) := by
  72  refine ⟨straight_null_geodesic ic, ?_, ?_⟩
  73  · simp [straight_null_geodesic, straight_line]
  74  · intro μ; simp [straight_null_geodesic, straight_line]
  75
  76theorem affine_reparametrization (g : MetricTensor) (geo : NullGeodesic g) (a b : ℝ)
  77    (ha : a ≠ 0) :
  78    let lam' := fun lam => a * lam + b
  79    ∃ geo' : NullGeodesic g, ∀ lam, geo'.path lam = geo.path (lam' lam) := by
  80  classical
  81  intro lam'
  82  refine ⟨{
  83    path := fun lam => geo.path (lam' lam)
  84    null_condition := ?null
  85    geodesic_equation := ?geoEq
  86  }, ?_⟩
  87  · intro lam
  88    simpa [lam'] using geo.null_condition (lam' lam)
  89  · intro lam μ
  90    simpa [lam'] using geo.geodesic_equation (lam' lam) μ
  91  · intro lam; rfl
  92
  93theorem minkowski_straight_line_is_geodesic (x₀ k : Fin 4 → ℝ)
  94    (h_null : Finset.sum (Finset.univ : Finset (Fin 4)) (fun μ =>
  95                Finset.sum (Finset.univ : Finset (Fin 4))
  96                  (fun ν =>
  97                    (inverse_metric minkowski_tensor) x₀
  98                      (fun i => if i.val = 0 then μ else ν) (fun _ => 0) *