OAI/Combinatorics/Progressions/Estimates/UnitVerticalMeanRowCorrelation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.expect_fin_two line 12
  2. theorem OAI.Erdos3.norm_correlation_partition_bound line 26
  3. theorem OAI.Erdos3.exists_dense_row_partition_correlation line 40
  4. def OAI.Erdos3.cyclicDivision line 117
  5. theorem OAI.Erdos3.cyclicDivision_val line 119
  6. theorem OAI.Erdos3.cyclicDivision_with_residue_injective line 123
  7. theorem OAI.Erdos3.expect_cyclicDivision_le line 136
  8. theorem OAI.Erdos3.expect_pair_cyclicDivision_le line 157
  9. def OAI.Erdos3.cyclicHalf line 190
  10. theorem OAI.Erdos3.cyclicHalf_val line 192
  11. theorem OAI.Erdos3.cyclicHalf_with_parity_injective line 196
  12. theorem OAI.Erdos3.expect_cyclicHalf_le line 206
  13. theorem OAI.Erdos3.expect_pair_cyclicHalf_le line 227
  14. def OAI.Erdos3.cyclicThird line 259
  15. theorem OAI.Erdos3.cyclicThird_val line 261
  16. theorem OAI.Erdos3.cyclicThird_with_residue_injective line 265
  17. theorem OAI.Erdos3.expect_cyclicThird_le line 275
  18. theorem OAI.Erdos3.expect_pair_cyclicThird_le line 296
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_unit_bounded_vertical_mean_row line 329
  20. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.test line 444
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.test_eval line 453
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.test_complexity line 458
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_unit_vertical_mean_row_model line 476