Physicslib4.Spacetime.LorentzCauchySchwarz

Reverse Cauchy-Schwarz inequality for timelike vectors

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

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

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

The abstract statement reverse_cauchy_schwarz_of_lorentzianAt only needs w to be timelike, which is stronger than the blueprint's lmm:reverse-cauchy-schwarz (stated symmetrically, with both v and w timelike); the specialisation Spacetime.reverse_cauchy_schwarz keeps the blueprint's symmetric hypotheses to match its statement. It depends only on the pointwise LorentzianAt condition, so it transfers verbatim to the metric g|_p of any spacetime.

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} (hw : (B w) w < 0) : (B v) v * (B w) w ≤ (B v) w ^ 2

Reverse Cauchy-Schwarz inequality for a timelike vector w of a symmetric Lorentzian bilinear form on a real four-dimensional vector space, and an arbitrary vector v. Only w needs to be timelike: this is stronger than the blueprint's lmm:reverse-cauchy-schwarz, which states the symmetric hypothesis v, w both timelike.

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. The hypothesis on v is kept (unused in the proof) to match the blueprint's symmetric statement of lmm:reverse-cauchy-schwarz; see reverse_cauchy_schwarz_of_lorentzianAt for the sharper form that only needs w timelike.