OAI/Probability/LatticeSurface/Convexity/HeatBath.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedData.compact_body line 142
2. lemma OAI.BoundedData.neighbor_nonempty line 160
3. def OAI.BoundedData.lower line 170
4. def OAI.BoundedData.upper line 174
5. lemma OAI.BoundedData.continuous_lower line 178
6. lemma OAI.BoundedData.continuous_upper line 183
7. lemma OAI.BoundedData.lower_le line 188
8. lemma OAI.BoundedData.le_upper line 195
9. lemma OAI.BoundedData.restore_update line 203
10. lemma OAI.BoundedData.update_body line 214
11. def OAI.BoundedData.update line 234
12. lemma OAI.BoundedData.update_mem line 238
13. lemma OAI.BoundedData.ascending_comparison line 246
14. lemma OAI.BoundedData.lower_fixed_comparison line 263