OAI/Analysis/IrrationalRotation/Couplings/CouplingMixture.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CouplingMixture.diagonal_fst line 14
2. lemma OAI.Invariant233.CouplingMixture.diagonal_snd line 18
3. instance OAI.Invariant233.CouplingMixture.diagonal_isProbabilityMeasure line 22
4. lemma OAI.Invariant233.CouplingMixture.fst_finsetSum line 27
5. lemma OAI.Invariant233.CouplingMixture.snd_finsetSum line 34
6. lemma OAI.Invariant233.CouplingMixture.mixture_fst line 41
7. lemma OAI.Invariant233.CouplingMixture.mixture_snd line 50
8. lemma OAI.Invariant233.CouplingMixture.mixture_isProbabilityMeasure line 60
9. lemma OAI.Invariant233.CouplingMixture.diagonal_ae line 69
10. lemma OAI.Invariant233.CouplingMixture.mixture_ae line 77
11. lemma OAI.Invariant233.CouplingMixture.withDensity_finite_mixture line 85
12. lemma OAI.Invariant233.CouplingMixture.intervalLaw_isProbabilityMeasure line 109
13. lemma OAI.Invariant233.CouplingMixture.intervalLaw_ae_mem line 117
14. lemma OAI.Invariant233.CouplingMixture.intervalLaw_pair_ordered line 120
15. lemma OAI.Invariant233.CouplingMixture.map_finsetSum line 131
16. lemma OAI.Invariant233.CouplingMixture.map_snd_label line 140
17. lemma OAI.Invariant233.CouplingMixture.map_label_event line 147
18. lemma OAI.Invariant233.CouplingMixture.labelledMixture_map_snd line 157
19. lemma OAI.Invariant233.CouplingMixture.labelledMixture_isProbabilityMeasure line 164
20. lemma OAI.Invariant233.CouplingMixture.labelledMixture_none_mass line 175
21. lemma OAI.Invariant233.CouplingMixture.labelledMixture_some_mass line 184
22. lemma OAI.Invariant233.CouplingMixture.cond_eq_withDensity_uniformDensity line 194
23. lemma OAI.Invariant233.CouplingMixture.ofReal_mixture_density line 209
24. lemma OAI.Invariant233.CouplingMixture.mixture_fst_real_density line 218
25. lemma OAI.Invariant233.CouplingMixture.mixture_snd_real_density line 229