OAI/Combinatorics/Progressions/Estimates/NativeMarkedDiagramOrbitLift.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.topQuotientOrbit line 18
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientOrbit_eval line 24
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientOrbit_cyclicOrbitPoint line 33
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientOrbit_surjective line 59
  5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_quotient_fiber_polynomialOrbit_lift line 106
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prescribed_marked_topQuotientOrbit_lift line 196
  7. def OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedMap line 265
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedMap_real_mk line 271
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedMap_mem_layer line 286
  10. def OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedOrbit line 294
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedOrbit_log line 303
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedOrbit_eq_iff line 309
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedOrbit_topQuotientOrbit line 323
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_marked_topQuotientOrbit_lift_of_quotient_eq line 339
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.refilteredMarkedMap_mem_layer line 388
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.refilteredMarkedMap_layer_surjective line 395
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_refiltered_prescribed_marked_topQuotientOrbit_lift line 412
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedMap_basis_logHeight line 473
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedMap_layer_surjective line 515
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedMap_real_layer_surjective line 529
  21. def OAI.Erdos3.RationalFilteredNilmanifold.markedTopQuotientDiagram line 562
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_marked_topQuotientOrbit_lift_diagram line 571
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_marked_topQuotientOrbit_lift_externalFamily line 590
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedOrbit_realEval line 616
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientMarkedOrbit_left_mul_of_map_eq_one line 628
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_marked_topQuotientOrbit_left_translated_lift_diagram line 652