OAI/Analysis/IrrationalRotation/Couplings/OneCoordinateCoupling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.OneCoordinateCoupling.baseLaw_isProbabilityMeasure line 14
2. lemma OAI.Invariant233.OneCoordinateCoupling.leftLaw_isProbabilityMeasure line 17
3. lemma OAI.Invariant233.OneCoordinateCoupling.rightLaw_isProbabilityMeasure line 25
4. lemma OAI.Invariant233.OneCoordinateCoupling.componentProbabilities_nonneg line 34
5. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_isProbabilityMeasure line 41
6. lemma OAI.Invariant233.OneCoordinateCoupling.replacement_ae_ordered line 67
7. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_ae_ordered line 78
8. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_fst line 84
9. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_snd line 93
10. lemma OAI.Invariant233.OneCoordinateCoupling.baseLaw_eq_restrict line 104
11. lemma OAI.Invariant233.OneCoordinateCoupling.interval_subset_unit line 107
12. lemma OAI.Invariant233.OneCoordinateCoupling.baseLaw_interval_measure line 112
13. lemma OAI.Invariant233.OneCoordinateCoupling.intervalLaw_eq_base_cond line 118
14. lemma OAI.Invariant233.OneCoordinateCoupling.intervalLaw_eq_base_withDensity line 126
15. lemma OAI.Invariant233.OneCoordinateCoupling.labelledLaw_map_snd line 135
16. lemma OAI.Invariant233.OneCoordinateCoupling.labelledLaw_isProbabilityMeasure line 139
17. lemma OAI.Invariant233.OneCoordinateCoupling.labelledLaw_tag_mass line 150
18. lemma OAI.Invariant233.OneCoordinateCoupling.labelledLaw_diagonal_mass line 159
19. lemma OAI.Invariant233.OneCoordinateCoupling.labelledLaw_ae_ordered line 163