theorem
proved
gradient_squared_minkowski
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Fields.Scalar on GitHub at line 83.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
80 (gradient φ x μ) * (gradient φ x ν)))
81
82/-- Gradient squared for Minkowski metric. -/
83theorem gradient_squared_minkowski (φ : ScalarField) (x : Fin 4 → ℝ) :
84 gradient_squared φ minkowski_tensor x =
85 -(gradient φ x 0)^2 + (gradient φ x 1)^2 + (gradient φ x 2)^2 + (gradient φ x 3)^2 := by
86 unfold gradient_squared
87 apply gradient_squared_minkowski_sum
88
89/-- Field squared. -/
90noncomputable def field_squared (φ : ScalarField) (x : Fin 4 → ℝ) : ℝ :=
91 (φ.ψ x) ^ 2
92
93theorem field_squared_nonneg (φ : ScalarField) (x : Fin 4 → ℝ) :
94 field_squared φ x ≥ 0 := by
95 simp [field_squared]
96 exact sq_nonneg _
97
98end Fields
99end Relativity
100end IndisputableMonolith