def
definition
einstein_hilbert_action
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Fields.Integration on GitHub at line 91.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
MetricTensor -
MetricTensor -
MetricTensor -
integrate_scalar -
VolumeElement -
ricci_scalar -
MetricTensor -
VolumeElement
used by
formal source
88
89
90/-- Einstein-Hilbert action: (M_P^2/2) ∫ √(-g) R d^4x. -/
91noncomputable def einstein_hilbert_action
92 (g : MetricTensor) (M_P_squared : ℝ) (vol : VolumeElement) : ℝ :=
93 (M_P_squared / 2) * integrate_scalar (ricci_scalar g) g vol
94
95/-- For Minkowski (R=0), EH action vanishes. -/
96theorem eh_action_minkowski (M_P_squared : ℝ) (vol : VolumeElement) :
97 einstein_hilbert_action minkowski_tensor M_P_squared vol = 0 := by
98 simp only [einstein_hilbert_action, integrate_scalar]
99 rw [Finset.sum_eq_zero]
100 · simp
101 · intro i _
102 simp [minkowski_ricci_scalar_zero]
103
104end Fields
105end Relativity
106end IndisputableMonolith