OAI/Analysis/IrrationalRotation/Couplings/PrefixHybrid.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductModel.prefixEndpoint_apply line 14
  2. theorem OAI.Invariant233.ProductModel.prefixPair_fst line 18
  3. theorem OAI.Invariant233.ProductModel.continuous_prefixEndpoint line 21
  4. theorem OAI.Invariant233.ProductModel.continuous_prefixPair line 31
  5. theorem OAI.Invariant233.ProductModel.measurable_prefixPair line 34
  6. theorem OAI.Invariant233.ProductModel.tendsto_prefixEndpoint line 37
  7. theorem OAI.Invariant233.ProductModel.tendsto_prefixPair line 45
  8. theorem OAI.Invariant233.ProductModel.prefixPairLaw_first_marginal line 49
  9. theorem OAI.Invariant233.ProductModel.prefixPairLaw_second_marginal line 54
  10. instance OAI.Invariant233.ProductModel.prefixPairLaw_finite line 60
  11. theorem OAI.Invariant233.ProductModel.prefixPairLaw_weaklyConverges line 65
  12. theorem OAI.Invariant233.ProductModel.ordered_selectedEndpoint line 82
  13. theorem OAI.Invariant233.ProductModel.prefixPairLaw_ordered line 90