OAI/NumberTheory/TwoPoint/Bounds/PhysicalMatrixComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compare physical matrix moments by their signed closed scalar words. Copy gates remain fixed while only the arithmetic origin is averaged.

  1. def OAI.TwoPointCorrelations.FiniteLaw.uniform line 15
  2. lemma OAI.TwoPointCorrelations.FiniteLaw.uniform_average line 20
  3. theorem OAI.TwoPointCorrelations.physicalMatrix_moment_comparison line 25