structure
definition
TimelikeGeodesic
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Geometry.MetricUnification on GitHub at line 121.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
118 (deriv (fun lam' => path lam' σ) lam))) = 0
119
120/-- A timelike geodesic: path with negative interval, using real Christoffel. -/
121structure TimelikeGeodesic (g : MetricTensor) extends RealGeodesic g where
122 timelike_condition : ∀ lam : ℝ,
123 Finset.sum Finset.univ (fun μ =>
124 Finset.sum Finset.univ (fun ν =>
125 g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
126 (deriv (fun lam' => path lam' μ) lam) *
127 (deriv (fun lam' => path lam' ν) lam))) < 0
128
129/-- A null geodesic using real Christoffel symbols. -/
130structure RealNullGeodesic (g : MetricTensor) extends RealGeodesic g where
131 null_condition : ∀ lam : ℝ,
132 Finset.sum Finset.univ (fun μ =>
133 Finset.sum Finset.univ (fun ν =>
134 g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
135 (deriv (fun lam' => path lam' μ) lam) *
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 +