structure
definition
def or abbrev
NullGeodesic
show as:
view Lean formalization →
formal statement (Lean)
20structure NullGeodesic (g : MetricTensor) where
21 path : ℝ → (Fin 4 → ℝ)
22 null_condition : ∀ lam : ℝ,
23 Finset.sum (Finset.univ : Finset (Fin 4)) (fun μ =>
24 Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
25 g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
26 (deriv (fun lam' => path lam' μ) lam) *
27 (deriv (fun lam' => path lam' ν) lam))) = 0
28 geodesic_equation : ∀ lam μ,
29 deriv (deriv (fun lam' => path lam' μ)) lam +
30 Finset.sum (Finset.univ : Finset (Fin 4)) (fun ρ =>
31 Finset.sum (Finset.univ : Finset (Fin 4)) (fun σ =>
32 (christoffel_from_metric g).Γ (path lam) μ ρ σ *
33 (deriv (fun lam' => path lam' ρ) lam) *
34 (deriv (fun lam' => path lam' σ) lam))) = 0
35
36/-- Initial conditions for null geodesic. -/