OAI/NumberTheory/TwoPoint/Bounds/ProjectedGraphTesting.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The deterministic bound for the manuscript's actual test vectors, with both degree cutoffs and the square-root padding weight.

  1. lemma OAI.TwoPointCorrelations.paddingTestVector_apply_norm_le line 14
  2. lemma OAI.TwoPointCorrelations.projected_paddingTestVector_support line 24
  3. lemma OAI.TwoPointCorrelations.paddingVertex_cut_bound line 36
  4. theorem OAI.TwoPointCorrelations.projected_padding_graph_test line 42