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