Reverse Cauchy-Schwarz inequality for timelike vectors

This file formalises the blueprint declaration lmm:reverse-cauchy-schwarz (Chapter 10, sections/sec10/10-2_spacetime).

For a symmetric Lorentzian bilinear form g (signature diag(-1,1,1,1)) and two timelike vectors v, w (i.e. g v v < 0, g w w < 0) the reverse Cauchy-Schwarz inequality holds:

g v v * g w w ≤ (g v w) ^ 2.

The abstract statement reverse_cauchy_schwarz_of_lorentzianAt depends only on the pointwise LorentzianAt condition, so it transfers verbatim to the metric g|_p of any spacetime; Spacetime.reverse_cauchy_schwarz is that specialisation.

Proof strategy

Expand v, w in a Lorentzian basis b, so g x y is the diagonal sum -(x⁰y⁰) + x¹y¹ + x²y² + x³y³ of the coordinates xⁱ = b.repr x i. The vector u = w⁰ • v - v⁰ • w has vanishing time coordinate, hence g u u ≥ 0; together with the algebraic identity

(w⁰)² * ((g v w)² - g v v * g w w)
  = (g v w * w⁰ - g w w * v⁰)² + (-(g w w)) * (g u u)

and w⁰ ≠ 0 (forced by g w w < 0) this gives the inequality.

theorem Physicslib4.reverse_cauchy_schwarz_of_lorentzianAt {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (_hsymm : ∀ (v w : V), (B v) w = (B w) v) (hL : LorentzianAt fun (v w : V) => (B v) w) {v w : V} (_hv : (B v) v < 0) (hw : (B w) w < 0) : (B v) v * (B w) w ≤ (B v) w ^ 2

Reverse Cauchy-Schwarz inequality for two timelike vectors of a symmetric Lorentzian bilinear form on a real four-dimensional vector space.

theorem Physicslib4.Spacetime.reverse_cauchy_schwarz (M : Spacetime) (x : M.Carrier) {v w : TangentSpace M.model x} (hv : M.IsTimelike v) (hw : M.IsTimelike w) : ((M.val x) v) v * ((M.val x) w) w ≤ ((M.val x) v) w ^ 2

Reverse Cauchy-Schwarz inequality for the metric of a spacetime: two timelike tangent vectors at a point satisfy g v v * g w w ≤ (g v w) ^ 2.