OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.ProductModel.EndpointPair line 13

    Also declared: ComparatorChallenges/IrrationalRotation.lean:667 (same declaration text).

  2. def OAI.Invariant233.ProductModel.selectedEndpoint line 15

    Also declared: ComparatorChallenges/IrrationalRotation.lean:669 (same declaration text).

  3. def OAI.Invariant233.ProductModel.triangularEvent line 18

    Also declared: ComparatorChallenges/IrrationalRotation.lean:672 (same declaration text).

  4. def OAI.Invariant233.ProductModel.triangularLaw line 21

    Also declared: ComparatorChallenges/IrrationalRotation.lean:675 (same declaration text).

  5. def OAI.Invariant233.ProductModel.triangularFirstDensity line 25

    Also declared: ComparatorChallenges/IrrationalRotation.lean:679 (same declaration text).

  6. def OAI.Invariant233.ProductModel.triangularSecondDensity line 28

    Also declared: ComparatorChallenges/IrrationalRotation.lean:682 (same declaration text).

  7. def OAI.Invariant233.ProductModel.TriangularLawProperties line 31

    Also declared: ComparatorChallenges/IrrationalRotation.lean:685 (same declaration text).

  8. def OAI.Invariant233.ProductModel.WeaklyConverges line 42

    Also declared: ComparatorChallenges/IrrationalRotation.lean:696 (same declaration text).

  9. def OAI.Invariant233.ProductModel.SupportedOnPositiveOrderedOrbitPairs line 46

    Also declared: ComparatorChallenges/IrrationalRotation.lean:700 (same declaration text).

  10. def OAI.Invariant233.ProductModel.HasUniformL2Marginals line 51

    Also declared: ComparatorChallenges/IrrationalRotation.lean:705 (same declaration text).

  11. def OAI.Invariant233.ProductModel.OrderedOrbitSampling line 58

    Also declared: ComparatorChallenges/IrrationalRotation.lean:712 (same declaration text).

  12. def OAI.Invariant233.ProductModel.HasAllFiniteCoordinateSampling line 64

    Also declared: ComparatorChallenges/IrrationalRotation.lean:718 (same declaration text).