OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.WeightedShift.diagonal_value line 14

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

2. theorem OAI.Invariant233.WeightedShift.diagonal_bound line 17

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

3. theorem OAI.Invariant233.WeightedShift.diagonal_aestronglyMeasurable line 22

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

4. def OAI.Invariant233.WeightedShift.fieldDiagonalVec line 43

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

5. theorem OAI.Invariant233.WeightedShift.fieldDiagonalVec_ae line 51

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

6. def OAI.Invariant233.WeightedShift.fieldDiagonalLinear line 59

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

7. def OAI.Invariant233.WeightedShift.fieldDiagonal line 82

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