OAI/Geometry/RCD/Coordinates/NormalizedPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identifying normalized Hilbert pairings with local test integrals

  1. theorem OAI.RegularPointCoordinates.normalizeLocalL2_smul line 15
  2. theorem OAI.RegularPointCoordinates.normalized_inner line 20
  3. theorem OAI.RegularPointCoordinates.normalized_inner_of_representatives line 33
  4. theorem OAI.RegularPointCoordinates.normalized_norm_le_of_bound line 42