theorem
proved
affine_reparametrization
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Geodesics.NullGeodesic on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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) *
99 k μ * k ν)) = 0) :
100 let path := fun lam => fun μ => x₀ μ + lam * k μ
101 ∃ geo : NullGeodesic minkowski_tensor,
102 (∀ lam, geo.path lam = path lam) := by
103 classical
104 intro path
105 have ic : InitialConditions := {
106 position := x₀