OAI/Analysis/IrrationalRotation/Model/ProductBase.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.circleRepresentative line 13

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

  2. instance OAI.Invariant233.circleMeasure_probability line 16

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

  3. abbrev OAI.Invariant233.ProductModel.Base line 22

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

  4. def OAI.Invariant233.ProductModel.baseMeasure line 24

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

  5. instance OAI.Invariant233.ProductModel.baseMeasure_probability line 26

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

  6. def OAI.Invariant233.ProductModel.Ordered line 30

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

  7. def OAI.Invariant233.ProductModel.rotation line 33

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

  8. def OAI.Invariant233.ProductModel.rotationIterate line 36

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

  9. def OAI.Invariant233.ProductModel.logarithmicCost line 39

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

  10. def OAI.Invariant233.ProductModel.weight line 42

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

  11. def OAI.Invariant233.ProductModel.JointlyRationallyIndependent line 45

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

  12. def OAI.Invariant233.ProductModel.AdmissibleAnglesAndCosts line 48

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

  13. abbrev OAI.Invariant233.ProductModel.Fiber line 52

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

  14. abbrev OAI.Invariant233.ProductModel.Hilbert line 53

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