OAI/Dynamics/ConditionalShuffle/CanonicalBridge.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Revealed.Split.slotEquiv line 9
2. lemma OAI.Revealed.Split.slotEquiv_apply line 12
3. lemma OAI.Revealed.Disintegration.average_quotient line 24
4. def OAI.Revealed.splitLayout line 42
5. lemma OAI.Revealed.splitLayout_post line 45
6. lemma OAI.Revealed.outsidePaths_split line 48
7. def OAI.Revealed.canonicalTransport line 60
8. lemma OAI.Revealed.canonical_realization line 67
9. lemma OAI.Revealed.expectedTV_completed line 82
10. theorem OAI.Revealed.expectedTV_le_instrument line 95
11. lemma OAI.Revealed.expectedTV_nonneg line 106