OAI/NumberTheory/TwoPoint/Bounds/PaddingWitnessProbability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Padding tests and the retained witness tests pay the missing reciprocal factors together.

  1. def OAI.TwoPointCorrelations.RetainedMainTests line 12
  2. theorem OAI.TwoPointCorrelations.retainedMainTests_congr line 18
  3. theorem OAI.TwoPointCorrelations.tuple_weight_mul_padding_hybrid_probability_le line 30