OAI/Combinatorics/Progressions/Nilpotent/NativeCoverNiltest.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice line 19
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_orbit line 28
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_normBound line 30
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_lipBound line 33
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_eval line 36
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_evalCyclic line 39
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_complexity line 42
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_unit_interval line 46
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onSublattice_vertical line 49
  10. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover line 78
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_log line 86
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_normBound line 89
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_lipBound line 92
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_eval line 95
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_evalCyclic line 98
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_complexity line 101
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_unit_interval line 105
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.onNativeCover_vertical line 108