OAI/Analysis/IrrationalRotation/Model/Product.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductModel.measurable_rep line 14

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

  2. theorem OAI.Invariant233.ProductModel.measurable_iterate line 17

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

  3. theorem OAI.Invariant233.ProductModel.measurable_cost line 28

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

  4. theorem OAI.Invariant233.ProductModel.weight_measurable line 37

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

  5. theorem OAI.Invariant233.ProductModel.weight_nonneg line 40

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

  6. theorem OAI.Invariant233.ProductModel.weight_le_one line 43

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

  7. def OAI.Invariant233.ProductModel.shiftOperator line 50

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

  8. def OAI.Invariant233.ProductModel.multiplierField line 53

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

  9. def OAI.Invariant233.ProductModel.multiplier line 60

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

  10. def OAI.Invariant233.ProductModel.multiplierGenerators line 66

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

  11. def OAI.Invariant233.ProductModel.factor line 70

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

  12. def OAI.Invariant233.ProductModel.traceVector line 73

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

  13. theorem OAI.Invariant233.ProductModel.measurable_complexWeight line 75

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

  14. theorem OAI.Invariant233.ProductModel.norm_complexWeight_le_one line 79

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

  15. def OAI.Invariant233.ProductModel.weightedOperator line 118

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