OAI/Analysis/IrrationalRotation/Sampling/ProductSampling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductModel.Sampling.representative_mem_Ico line 12
  2. theorem OAI.Invariant233.ProductModel.Sampling.representative_measurable line 16
  3. theorem OAI.Invariant233.ProductModel.Sampling.selectedEndpoint_measurable line 20
  4. theorem OAI.Invariant233.ProductModel.Sampling.endpointMap_measurable line 29
  5. theorem OAI.Invariant233.ProductModel.Sampling.triangularEvent_measurable line 33
  6. theorem OAI.Invariant233.ProductModel.Sampling.ordered_measurable line 44
  7. theorem OAI.Invariant233.ProductModel.Sampling.triangularLaw_finite line 53
  8. theorem OAI.Invariant233.ProductModel.Sampling.triangularLaw_ordered line 57
  9. theorem OAI.Invariant233.ProductModel.Sampling.triangular_density_bounds line 67
  10. theorem OAI.Invariant233.ProductModel.Sampling.circleMeasure_singleton line 80
  11. theorem OAI.Invariant233.ProductModel.Sampling.representative_map_haar line 84
  12. theorem OAI.Invariant233.ProductModel.Sampling.representative_tail_measure line 88
  13. theorem OAI.Invariant233.ProductModel.Sampling.representative_initial_measure line 92
  14. theorem OAI.Invariant233.ProductModel.Sampling.upper_box_measure line 96
  15. theorem OAI.Invariant233.ProductModel.Sampling.lower_box_measure line 101
  16. theorem OAI.Invariant233.ProductModel.Sampling.triangularLaw_first_marginal line 106
  17. theorem OAI.Invariant233.ProductModel.Sampling.reversedRestriction_first_marginal line 111