OAI/Combinatorics/Progressions/Nilpotent/NiltestComplement.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realificationLieHom_id_apply line 11
  2. def OAI.Erdos3.RationalFilteredNilmanifold.raiseStepProjection line 25
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStepProjection_mk line 33
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStepProjection_lipschitz line 44
  5. def OAI.Erdos3.RationalFilteredNilmanifold.raiseStepRealOrbit line 65
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStepRealOrbit_log line 70
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStepProjection_orbit line 74
  8. def OAI.Erdos3.raisedNiltestBudget line 97
  9. theorem OAI.Erdos3.le_raisedNiltestBudget line 99
  10. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep line 112
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep_eval line 123
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep_evalCyclic line 131
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep_unit_interval line 136
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep_complexity line 139
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep_top_vertical line 185
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStep_top_subgroup_eq_bot line 212
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStep_observable_top_vertical line 224
  18. theorem OAI.Erdos3.cyclic_upperComparison_mul_niltest line 249
  19. inductive OAI.Erdos3.PositiveCyclicNiltest line 327
  20. theorem OAI.Erdos3.PositiveCyclicNiltest.unit_interval line 342
  21. theorem OAI.Erdos3.PositiveCyclicNiltest.mono line 349
  22. theorem OAI.Erdos3.PositiveCyclicNiltest.mul_upperComparison line 355
  23. theorem OAI.Erdos3.PositiveCyclicNiltest.apply_shiftBound line 368
  24. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.complement line 398
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.complement_evalCyclic line 414
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.complement_unitInterval line 417
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.complement_complexity line 426
  28. theorem OAI.Erdos3.PositiveCyclicNiltest.complement line 437
  29. theorem OAI.Erdos3.CyclicNiltestUpperComparison.test_positive line 446