OAI/Combinatorics/Progressions/Nilpotent/CanonicalReducedMajorTwistedNiltest.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.PolynomialTranslationLie.majorZeroParameterSlice_eq line 14
  2. theorem OAI.Erdos3.PolynomialTranslationLie.majorZeroParameterSlice_mass line 20
  3. theorem OAI.Erdos3.PolynomialTranslationLie.majorZeroParameterSlice_degree line 26
  4. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_buffered_niltest line 45
  5. theorem OAI.Erdos3.fractionalCoefficientPolynomial_mem_weightedSupportLE line 86
  6. theorem OAI.Erdos3.fractionalCoefficientPolynomial_mass_le_of_weightedSupportLE line 100
  7. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_degree_reduced_niltest line 119
  8. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_reduced_niltest line 222
  9. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_twisted_niltest line 334
  10. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_reduced_twisted_niltest line 368
  11. theorem OAI.Erdos3.PolynomialTranslationLie.fractionalMajorPolynomial_support line 478
  12. theorem OAI.Erdos3.PolynomialTranslationLie.fractionalMajorPolynomial_mass line 486
  13. def OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest line 509
  14. theorem OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest_normBound line 533
  15. theorem OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest_lipBound line 536
  16. theorem OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest_orbit line 540
  17. theorem OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest_observable line 544
  18. theorem OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest_evalReal line 548
  19. theorem OAI.Erdos3.PolynomialTranslationLie.reducedMajorTranslationTwistedNiltest_eval line 567
  20. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reducedMajorTranslationTwistedNiltest_complexity line 589