OAI/NumberTheory/TwoPoint/Bounds/PaddingRetainedProbability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Under the exact harmonic padding law, more than half the mass obeys both the degree and logarithmic-size restrictions used to form the bins.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.probability_lt_le_average line 14
  2. lemma OAI.TwoPointCorrelations.FiniteLaw.probability_and_ge line 29
  3. lemma OAI.TwoPointCorrelations.booleanCount_nonneg line 40
  4. lemma OAI.TwoPointCorrelations.paddingLog_nonneg line 45
  5. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_reciprocal_padding_count_mean line 52
  6. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_retained_padding_probability line 61