OAI/Combinatorics/Progressions/Estimates/UnconditionalStepDrop.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.frozen_refiltered_top_invariant line 23
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.frozen_refiltered_coset_invariant line 50
  3. theorem OAI.Erdos3.exists_real_module_topology line 78
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.symbol_of_native line 99
  5. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.frozen_coset_top_invariant line 131
  6. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.frozen_group_invariant line 175
  7. theorem OAI.Erdos3.exists_prepared_antisymmetric_descent line 200
  8. theorem OAI.Erdos3.exists_antisymmetric_frozen_descent line 310
  9. def OAI.Erdos3.NativePolynomialOrbitFactors.frozenMiddleValue line 382
  10. theorem OAI.Erdos3.exists_native_frozen_middle_expansion line 389
  11. theorem OAI.Erdos3.exists_antisymmetric_orbit_approximation line 458
  12. theorem OAI.Erdos3.exists_translated_step_drop_succ line 514
  13. theorem OAI.Erdos3.exists_translated_step_drop line 580