OAI/Combinatorics/Progressions/Estimates/AllocatedMarkedDictionaryRecovery.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_id_eq_changeStep line 13
  2. def OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverMap line 36
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverMap_mk line 46
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverMap_surjective line 54
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverMap_lipschitz line 65
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverMap_orbit line 91
  7. def OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverPullback line 118
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverPullback_mk line 121
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverPullback_orbit line 128
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCoverPullback_bounds line 137
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_split_reconstruction_cover line 170
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_lowered_split_reconstruction_cover line 272
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_frozen_split_reconstruction line 402
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_diagram_native_external_net line 550
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_frozen_two_target_reconstruction line 684
  16. def OAI.Erdos3.RationalFilteredNilmanifold.AllocatedMarkedDiagramRecoveryCovers line 889
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_allocated_marked_diagram_recovery_covers line 919
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeGridRightDictionary.markedTopQuotient_recovery line 1049
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.AllocatedMarkedDiagramRecoveryCovers.of_nativeGridRightDictionary line 1102