OAI/NumberTheory/TwoPoint/Bounds/WeightedMatrixTest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Deterministic testing of a weighted matrix. Only rows on the support of the test vector enter the estimate.

  1. lemma OAI.TwoPointCorrelations.weighted_matrix_test_le line 13
  2. lemma OAI.TwoPointCorrelations.weighted_matrix_test_uniform line 41