OAI/NumberTheory/TwoPoint/Bounds/MainPaddingTests.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual main-word padding tests imply all tests retained after tuple centering.

  1. def OAI.TwoPointCorrelations.MainPaddingTests line 12
  2. theorem OAI.TwoPointCorrelations.mainPaddingTests_retained line 17
  3. theorem OAI.TwoPointCorrelations.mainPaddingTests_congr line 29
  4. def OAI.TwoPointCorrelations.paddingWeightedFunction line 42
  5. lemma OAI.TwoPointCorrelations.paddingWeightedFunction_nonneg line 46
  6. lemma OAI.TwoPointCorrelations.paddingWeightedFunction_le line 55
  7. theorem OAI.TwoPointCorrelations.paddingWeightedFunction_retained line 64
  8. theorem OAI.TwoPointCorrelations.paddingWeightedFunction_invariant line 75