def definition def or abbrev

`einstein_hilbert_action`

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

formal statement (Lean)

  91noncomputable def einstein_hilbert_action
  92  (g : MetricTensor) (M_P_squared : ℝ) (vol : VolumeElement) : ℝ :=

Definition body.

  93  (M_P_squared / 2) * integrate_scalar (ricci_scalar g) g vol
  94
  95/-- For Minkowski (R=0), EH action vanishes. -/

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

eh_action_minkowski in IndisputableMonolith.Relativity.Fields.Integration decl_use

Lean names referenced from this declaration's body.

MetricTensor in IndisputableMonolith.Foundation.Hamiltonian decl_use
MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
integrate_scalar in IndisputableMonolith.Relativity.Fields.Integration decl_use
VolumeElement in IndisputableMonolith.Relativity.Fields.Integration decl_use
ricci_scalar in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
MetricTensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use
VolumeElement in IndisputableMonolith.Relativity.ILG.Action decl_use