OAI/Dynamics/ConditionalShuffle/InstrumentTV.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Revealed.Instrument.pathJoint_marginal line 12
2. lemma OAI.Revealed.Instrument.conditional_pathJoint line 18
3. def OAI.Revealed.Instrument.distance line 25
4. lemma OAI.Revealed.Instrument.distance_disintegration line 29
5. lemma OAI.Revealed.Instrument.distance_joint line 39
6. lemma OAI.Revealed.Instrument.distance_nonneg line 45
7. lemma OAI.Revealed.Instrument.realConv_uniform line 48
8. lemma OAI.Revealed.Instrument.distance_succ_le line 53
9. lemma OAI.Revealed.Instrument.distance_antitone line 75
10. def OAI.Revealed.Instrument.costs line 78
11. lemma OAI.Revealed.Instrument.costs_sum_le line 82
12. lemma OAI.Revealed.Instrument.costs_kernels line 107
13. def OAI.Revealed.Instrument.block line 118
14. lemma OAI.Revealed.Instrument.block_joint line 123
15. lemma OAI.Revealed.Instrument.block_probability line 128