theorem proved term proof

`spatialNormSq_nonneg`

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

formal statement (Lean)

 131theorem spatialNormSq_nonneg (x : Fin 4 → ℝ) : 0 ≤ spatialNormSq x := by

Term-mode proof.

 132  unfold spatialNormSq
 133  positivity
 134

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

differentiableAt_coordRay_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
laplacian_radialInv_n in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
laplacian_radialInv_zero_no_const in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_spatialRadius in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
spatialRadius_coordRay_ne_zero in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
spatialRadius_ne_zero_iff in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
spatialRadius_pos_of_ne_zero in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
laplacian_radialInv_n_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
laplacian_radialInv_zero_no_const_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
partialDeriv_v2_spatialRadius_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
spatialRadius_coordRay_ne_zero_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use

Lean names referenced from this declaration's body.

spatialNormSq in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use