structure
definition
RealGeodesic
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 110.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
107
108/-- A geodesic using the real Christoffel symbols from `Curvature.christoffel`.
109 This is the physically correct geodesic equation. -/
110structure RealGeodesic (g : MetricTensor) where
111 path : ℝ → (Fin 4 → ℝ)
112 geodesic_equation : ∀ lam μ,
113 deriv (deriv (fun lam' => path lam' μ)) lam +
114 Finset.sum Finset.univ (fun ρ =>
115 Finset.sum Finset.univ (fun σ =>
116 christoffel g (path lam) μ ρ σ *
117 (deriv (fun lam' => path lam' ρ) lam) *
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 : ℝ,