OAI/Analysis/IrrationalRotation/Sampling/ProductPrefixApproximation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductPrefixApproximation.tendstoUniformly_pi_iff line 19
  2. def OAI.Invariant233.ProductPrefixApproximation.freeze line 30
  3. theorem OAI.Invariant233.ProductPrefixApproximation.continuous_freeze line 33
  4. theorem OAI.Invariant233.ProductPrefixApproximation.freeze_tendstoUniformly line 41
  5. theorem OAI.Invariant233.ProductPrefixApproximation.continuous_freeze_tendstoUniformly line 49
  6. def OAI.Invariant233.ProductPrefixApproximation.Endpoint.freeze line 60
  7. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.continuous_freeze line 64
  8. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.freeze_tendstoUniformly line 69
  9. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.continuous_freeze_tendstoUniformly line 75
  10. abbrev OAI.Invariant233.ProductPrefixApproximation.Endpoint.FinitePair line 81
  11. def OAI.Invariant233.ProductPrefixApproximation.Endpoint.restrict line 83
  12. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.continuous_restrict line 86
  13. def OAI.Invariant233.ProductPrefixApproximation.Endpoint.extend line 90
  14. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.continuous_extend line 94
  15. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.extend_restrict line 114
  16. def OAI.Invariant233.ProductPrefixApproximation.Endpoint.finiteTest line 119
  17. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.finiteTest_restrict line 123
  18. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.exists_finiteTest_uniformly_near line 128
  19. theorem OAI.Invariant233.ProductPrefixApproximation.Endpoint.freeze_zero line 136