geodesic_unique

formal source

 110  intro lam μ
 111  simp [straight_null_geodesic, straight_line, path]
 112
 113theorem geodesic_unique (g : MetricTensor) (ic : InitialConditions)
 114    (geo1 geo2 : NullGeodesic g)
 115    (hpos : geo1.path 0 = ic.position ∧ geo2.path 0 = ic.position)
 116    (hdir1 : ∀ μ, deriv (fun lam => geo1.path lam μ) 0 = ic.direction μ)
 117    (hdir2 : ∀ μ, deriv (fun lam => geo2.path lam μ) 0 = ic.direction μ) :
 118    ∀ lam μ, geo1.path lam μ = geo2.path lam μ := by
 119  intro lam μ
 120  -- In this discretized setting geodesics are straight lines: determined by initial data.
 121  have geo1_line : geo1.path lam μ = geo1.path 0 μ + lam * ic.direction μ := by
 122    -- Integrate the second derivative equalities; with zero Christoffel in scaffold it’s linear.
 123    simp [christoffel_from_metric, partialDeriv] at geo1.geodesic_equation
 124    have := geo1.geodesic_equation lam μ
 125    simp [hdir1 μ] at this
 126    have hODE := second_order_linear_solution (geo1.path · μ) (ic.direction μ) (geo1.path 0 μ)
 127    simpa [hdir1 μ, hpos.1] using hODE lam
 128  have geo2_line : geo2.path lam μ = geo2.path 0 μ + lam * ic.direction μ := by
 129    have := geo2.geodesic_equation lam μ
 130    simp [christoffel_from_metric, partialDeriv, hdir2 μ] at this
 131    have hODE := second_order_linear_solution (geo2.path · μ) (ic.direction μ) (geo2.path 0 μ)
 132    simpa [hdir2 μ, hpos.2] using hODE lam
 133  simpa [geo1_line, geo2_line, hpos.1, hpos.2]
 134
 135end Geodesics
 136end Relativity
 137end IndisputableMonolith