OAI/Combinatorics/Progressions/Estimates/AxisCompression.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedAxisProduct line 14
  2. theorem OAI.Erdos3.orderedProduct_normalized_telescope line 17
  3. theorem OAI.Erdos3.normalizedAxisProduct_tested_le line 30
  4. theorem OAI.Erdos3.normalizedAxisProduct_bounds line 59
  5. theorem OAI.Erdos3.exists_native_cyclic_small_modulus_correlation line 77
  6. theorem OAI.Erdos3.exists_adapted_basis_of_shift_failure line 136
  7. theorem OAI.Erdos3.exists_mixed_primitive_correlation_large_modulus line 174
  8. theorem OAI.Erdos3.exists_cyclicNativeInverse_step line 243
  9. theorem OAI.Erdos3.exists_cyclicNativeInverse_add_two line 271
  10. theorem OAI.Erdos3.exists_cyclicNativeInverse_ge_two line 279
  11. theorem OAI.Erdos3.exists_cyclicNativeInverse_positive line 292
  12. theorem OAI.Erdos3.exists_native_inverse_on_cyclic_encoding line 318
  13. theorem OAI.Erdos3.exists_native_detector_of_gowers line 373
  14. theorem OAI.Erdos3.PositiveShiftBasis.exists_testingFamily_native_detectors line 442
  15. theorem OAI.Erdos3.PositiveShiftBasis.exists_bounded_testingFamily_native_detectors line 479
  16. theorem OAI.Erdos3.CyclicNiltestUpperComparison.mono_budget line 555
  17. theorem OAI.Erdos3.cyclic_difference_norm_bound line 563
  18. theorem OAI.Erdos3.PositiveShiftBasis.exists_bounded_native_contradiction line 586
  19. theorem OAI.Erdos3.exists_cyclicShiftComparison_step line 632
  20. theorem OAI.Erdos3.exists_cyclicShiftComparison_succ line 661
  21. theorem OAI.Erdos3.exists_cyclicShiftComparison_positive line 673
  22. def OAI.Erdos3.CyclicTranslatedNiltestShiftBound line 690
  23. theorem OAI.Erdos3.exists_cyclicShiftComparison_translated line 695
  24. theorem OAI.Erdos3.exists_axis_compression line 764