OAI/NumberTheory/TwoPoint/Bounds/BoundedPaddingUnion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite witness union includes all record lengths and all original main words.

  1. theorem OAI.TwoPointCorrelations.main_sum_bounded_padding_union_probability_le line 13
  2. theorem OAI.TwoPointCorrelations.weighted_supported_padding_averages_le_catalog line 47