pith. machine review for the scientific record. sign in
theorem proved term proof

kinetic_nonneg

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)

  78theorem kinetic_nonneg (φ : ScalarField) (g : MetricTensor) (vol : VolumeElement)
  79    (hSign : ∀ x, 0 ≤ gradient_squared φ g x) :
  80  0 ≤ kinetic_action φ g vol := by

proof body

Term-mode proof.

  81  unfold kinetic_action integrate_scalar sqrt_minus_g
  82  apply mul_nonneg (by norm_num)
  83  apply mul_nonneg (pow_nonneg (le_of_lt vol.grid_spacing_pos) 4)
  84  apply Finset.sum_nonneg
  85  intro i _
  86  apply mul_nonneg (by norm_num : (0 : ℝ) ≤ 1)
  87  apply hSign
  88
  89
  90/-- Einstein-Hilbert action: (M_P^2/2) ∫ √(-g) R d^4x. -/

depends on (13)

Lean names referenced from this declaration's body.