OAI/Probability/LatticeSurface/Convexity/MetropolisSupport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BrownianForcing.acceptedShiftMeasure line 10
2. def OAI.BrownianForcing.acceptedShiftPair line 14
3. def OAI.BrownianForcing.metropolisShiftPair line 19
4. lemma OAI.BrownianForcing.acceptedShift_translate_le line 29
5. lemma OAI.BrownianForcing.acceptedShiftPair_fst line 39
6. lemma OAI.BrownianForcing.acceptedShiftPair_fst_le line 53
7. lemma OAI.BrownianForcing.acceptedShiftPair_swap line 63
8. lemma OAI.BrownianForcing.metropolisShiftPair_fst line 72
9. lemma OAI.BrownianForcing.metropolisShiftPair_swap line 84
10. lemma OAI.BrownianForcing.metropolisShiftPair_snd line 93
11. lemma OAI.BrownianForcing.metropolisShiftPair_probability line 101