OAI/NumberTheory/TwoPoint/Bounds/ShiftMatrixTranslation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Translate the physical block coordinates without changing its matrix. Arithmetic weights and the numerical gate use the same origin.

  1. theorem OAI.TwoPointCorrelations.physicalShiftMatrix_translate line 13
  2. theorem OAI.TwoPointCorrelations.physicalBlockMatrix_eq_integer line 54