OAI/Combinatorics/Progressions/Estimates/NativeOptionOriginalOrbit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Erdos3.optionRealificationTopology line 17
  2. instance OAI.Erdos3.optionRealificationTopologicalAddGroup line 24
  3. instance OAI.Erdos3.optionRealificationContinuousSMul line 32
  4. instance OAI.Erdos3.optionRealificationT2Space line 40
  5. def OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalSpaceProjection line 67
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalSpaceProjection_mk line 70
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalSpaceProjection_piRealOrbit line 74
  8. def OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable line 84
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_apply line 88
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_piRealOrbit line 93
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_score line 104
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalSpaceProjection_lipschitz line 126
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalProjection_layers line 155
  14. def OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit line 161
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_log line 171
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_eval line 182
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_value line 193
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_piRealOrbit line 202
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_score line 214
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_mark_eval line 225
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalOrbit_mark_log line 253