OAI/Analysis/IrrationalRotation/Sampling/PrefixDomination.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CouplingMixture.intervalLaw_pair_strictly_ordered line 13
2. instance OAI.Invariant233.OneCoordinateCoupling.triangleLaw_isFiniteMeasure line 30
3. lemma OAI.Invariant233.OneCoordinateCoupling.replacement_ae_strictly_ordered line 34
4. lemma OAI.Invariant233.OneCoordinateCoupling.replacementDensity_measurable line 42
5. lemma OAI.Invariant233.OneCoordinateCoupling.replacement_eq_triangle_withDensity line 52
6. lemma OAI.Invariant233.OneCoordinateCoupling.replacement_absolutelyContinuous_triangle line 75
7. lemma OAI.Invariant233.OneCoordinateCoupling.componentLaw_absolutelyContinuous line 82
8. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_absolutelyContinuous_diagonal_add_triangle line 89
9. lemma OAI.Invariant233.OneCoordinateCoupling.finite_pairLaws_domination line 102