OAI/Combinatorics/Progressions/Nilpotent/RankAdaptedNiltest.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest line 18
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_orbit line 42
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_normBound line 44
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_eval line 46
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_evalCyclic line 48
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_unit_interval line 51
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_vertical line 54
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_kernel_invariant line 62
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.rebaseNiltest_complexity line 69
  10. def OAI.Erdos3.rankAdaptedNiltestBase line 98
  11. def OAI.Erdos3.rankAdaptedNiltestBudget line 100
  12. theorem OAI.Erdos3.le_rankAdaptedNiltestBudget line 103
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.exists_adapted_niltest line 114