`BookProof.ChapterGravityMetric.reverse_cauchy_schwarz` (v x : Fin 4 → ℝ) (hv : minkSq v = -1) : 0 ≤ (∑ a, x a * lower v a) ^ 2 + minkSq x

Initializing...

`BookProof.ChapterGravityMetric.reverse_cauchy_schwarz` (v x : Fin 4 → ℝ) (hv : minkSq v = -1) : 0 ≤ (∑ a, x a * lower v a) ^ 2 + minkSq x · Prove2Me