OAI/Geometry/EinsteinFour/CP2WeightedBessel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bessel's inequality for the two orthogonal directions used in the projective midpoint construction.

  1. def OAI.PositiveEinsteinFour.cp2Normalize line 15
  2. theorem OAI.PositiveEinsteinFour.cp2Normalize_norm line 18
  3. theorem OAI.PositiveEinsteinFour.cp2Normalize_inner_norm line 22
  4. theorem OAI.PositiveEinsteinFour.cp2_weighted_bessel line 27