OAI/Combinatorics/Progressions/Nilpotent/IdealInvariantNiltestBudget.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.UnitIntervalValued line 20
  2. def OAI.Erdos3.CyclicNiltestUpperComparison line 25
  3. def OAI.Erdos3.RationalFilteredNilmanifold.idealQuotientOrbit line 51
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.idealQuotientOrbit_eval line 57
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_idealInvariant_niltest line 70
  6. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.intervalClip line 144
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.intervalClip_unitInterval line 165
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.intervalClip_complexityLE line 169
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.intervalClip_eval line 172
  10. def OAI.Erdos3.RationalFilteredNilmanifold.cyclicOrbitPoint line 195
  11. def OAI.Erdos3.RationalFilteredNilmanifold.sectionNiltest line 201
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.sectionNiltest_unit_interval line 227
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.sectionNiltest_complexityLE line 235
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.sectionNiltest_evalCyclic_re line 247
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.sectionNiltest_none_eval line 255
  16. def OAI.Erdos3.CyclicNiltestShiftBound line 271
  17. theorem OAI.Erdos3.cyclicNiltestShiftBound_zero_of_constants line 280
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.UnitIntervalValued.norm_le_one line 310
  19. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.withUnitBound line 319
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.withUnitBound_orbit line 322
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.withUnitBound_eval line 325
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.withUnitBound_complexity line 328
  23. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.positiveLocalization line 357
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.positiveLocalization_orbit line 376
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.positiveLocalization_unit_interval line 379
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.positiveLocalization_eval_re line 385
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.positiveLocalization_support line 390
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.positiveLocalization_complexity line 400
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_idealInvariant_niltest_budget line 424