structure
definition
def or abbrev
TimelikeGeodesic
show as:
view Lean formalization →
formal statement (Lean)
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. -/