OAI/Combinatorics/Progressions/Estimates/TranslationMajorTwistedCorrelationStepDrop.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.PolynomialTranslationLie.exists_translation_major_vertical_selection line 16
  2. abbrev OAI.Erdos3.RationalFilteredNilmanifold.PairAlgebra line 104
  3. def OAI.Erdos3.RationalFilteredNilmanifold.pairModels line 106
  4. def OAI.Erdos3.RationalFilteredNilmanifold.pairFrequencies line 112
  5. def OAI.Erdos3.RationalFilteredNilmanifold.pairFrequency line 117
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairFrequency_apply line 120
  7. def OAI.Erdos3.RationalFilteredNilmanifold.pairOrbit line 128
  8. def OAI.Erdos3.RationalFilteredNilmanifold.pairOrbitSymbol line 134
  9. def OAI.Erdos3.RationalFilteredNilmanifold.pairTests line 148
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairTests_complexity line 153
  11. def OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest line 168
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest_eval line 175
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest_complexity line 181
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest_orbit line 188
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest_symbol line 192
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest_orbit_eq line 200
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairNiltest_symbol_eq_of_orbit_eq line 209
  18. theorem OAI.Erdos3.exists_native_pair_vertical_step_drop line 226
  19. theorem OAI.Erdos3.pairFrequency_logHeight line 303
  20. theorem OAI.Erdos3.exists_native_pair_positive_step_drop line 318
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairOrbitSymbol_eq_of_right_symbol_eq line 433
  22. theorem OAI.Erdos3.PolynomialTranslationLie.exists_translation_major_correlation_step_drop line 503
  23. theorem OAI.Erdos3.PolynomialTranslationLie.exists_translation_major_twisted_correlation_step_drop line 591