OAI/Combinatorics/Progressions/Estimates/CommonIntegralModelEquivalences.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_common_height_bounded_subalgebra line 20
  2. theorem OAI.Erdos3.exists_common_log_height_subalgebra line 32
  3. theorem OAI.Erdos3.exists_common_log_height_basis_subalgebra line 45
  4. theorem OAI.Erdos3.common_subalgebra_cost_le_budget line 56
  5. theorem OAI.Erdos3.exists_common_fast_subalgebra line 70
  6. theorem OAI.Erdos3.exists_common_fast_basis_subalgebra line 86
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_fast_relative line 115
  8. theorem OAI.Erdos3.exists_common_bounded_moduli line 148
  9. theorem OAI.Erdos3.exists_common_subalgebra_and_moduli line 187
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_reduced_fast_relative line 244
  11. theorem OAI.Erdos3.exists_common_positive_nat line 277
  12. theorem OAI.Erdos3.exists_common_fast_subalgebra_and_denominator line 291
  13. theorem OAI.Erdos3.NilpotentLieFiltration.mem_reduced_fast_diagonal_iff line 333
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_synchronized_reduced_fast_factors line 344
  15. theorem OAI.Erdos3.NilpotentLieFiltration.synchronized_reduced_fast_relative line 366
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_integral_models line 390
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_integral_model_equivalences line 451