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

L_density

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)

  69noncomputable def L_density (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ :=

proof body

Definition body.

  70  (p.alpha ^ 2) / 2 - (p.cLag ^ 2) / 2 + p.cLag * p.alpha
  71
  72/-- Covariant scalar Lagrangian pieces (symbolic). -/

depends on (4)

Lean names referenced from this declaration's body.