OAI/Probability/LatticeSurface/Convexity/BrunnMinkowski.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FacetVolume.distanceApprox line 17
2. lemma OAI.FacetVolume.continuous_distanceApprox line 20
3. lemma OAI.FacetVolume.distanceApprox_pos line 24
4. lemma OAI.FacetVolume.distanceApprox_le_one line 27
5. lemma OAI.FacetVolume.tendsto_distanceApprox line 32
6. lemma OAI.FacetVolume.tendsto_cubeIntegral_distanceApprox line 45
7. lemma OAI.FacetVolume.infDist_weighted_combination line 64
8. lemma OAI.FacetVolume.distanceApprox_combination line 80
9. theorem OAI.FacetVolume.compact_volume_bm_in_cube line 90
10. theorem OAI.FacetVolume.compact_volume_brunn_minkowski line 107