OAI/Combinatorics/Progressions/Estimates/ControlledComparisonModel.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_model_of_bounded_embedding line 16
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.embedding_basis_card_le line 70
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_model_of_embedding_logHeight line 76
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_dilationPair_layer_basis line 117
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_dilationPair_filtration_basis line 139
  6. def OAI.Erdos3.pairToPi line 168
  7. theorem OAI.Erdos3.pairToPi_zero line 171
  8. theorem OAI.Erdos3.pairToPi_one line 173
  9. theorem OAI.Erdos3.pairToPi_injective line 175
  10. def OAI.Erdos3.NilpotentLieFiltration.dilationPairToPi line 183
  11. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairToPi_injective line 186
  12. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairToPi_mem line 189
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.pair_product_basis_logHeight line 204
  14. def OAI.Erdos3.RationalFilteredNilmanifold.dilationPairLattice line 231
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.dilationPairLattice_mem line 235
  16. def OAI.Erdos3.RationalFilteredNilmanifold.dilationPairGeometryBudget line 250
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_dilationPair_model line 253
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_dilationPair_model_of_eq line 329
  19. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationPairLattice line 349
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationPairLattice_mem line 354
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_dilationPair_model line 370
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_comparison_layer_basis line 399
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_comparison_filtration_basis line 411
  24. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonGeometryBudget line 446
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonSubalgebra_finrank_le line 449
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_comparison_model line 464
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_comparisonModel_cost line 516
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_comparison_model line 546