pith. machine review for the scientific record. sign in
def definition def or abbrev

christoffel

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  13noncomputable def christoffel (g : MetricTensor) : (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ :=

proof body

Definition body.

  14  fun x rho mu nu =>
  15    (1/2 : ℝ) * Finset.univ.sum (fun (lambda : Fin 4) =>
  16      (inverse_metric g) x (fun _ => rho) (fun _ => lambda) * (
  17        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else lambda)) nu x) +
  18        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then nu else lambda)) mu x) -
  19        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else nu)) lambda x)
  20      ))
  21
  22/-- Christoffel symbols are symmetric in the lower indices (torsion-free). -/

used by (30)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.