OAI/Probability/LatticeSurface/Convexity/HeatBathGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedData.lower_update line 15
2. lemma OAI.BoundedData.upper_update line 25
3. lemma OAI.BoundedData.split_inv_update line 36
4. lemma OAI.BoundedData.continuous_update line 51
5. lemma OAI.BoundedData.split_body_region line 64
6. lemma OAI.BoundedData.lower_bound_difference line 137
7. lemma OAI.BoundedData.upper_bound_difference line 152
8. lemma OAI.BoundedData.update_bound_difference line 167
9. lemma OAI.BoundedData.update_norm_difference line 184
10. lemma OAI.BoundedData.update_sum line 193