OAI/NumberTheory/TwoPoint/Walks/BlockTesting.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Test the retained graph against bounded arithmetic functions. The norm average uses the truncated integer padding estimate.

  1. lemma OAI.TwoPointCorrelations.norm_inner_operator_le line 15
  2. theorem OAI.TwoPointCorrelations.FiniteLaw.average_operator_test line 24
  3. def OAI.TwoPointCorrelations.paddingTestVector line 49
  4. lemma OAI.TwoPointCorrelations.paddingTestVector_norm_sq_le line 54
  5. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_padding_test_norm line 71
  6. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_padding_test_progression_norm line 100
  7. lemma OAI.TwoPointCorrelations.projected_paddingTestVector_norm_sq_le line 124