OAI/Probability/LatticeSurface/Convexity/SliceGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FacetVolume.slice line 18
  2. def OAI.FacetVolume.sliceVolume line 21
  3. lemma OAI.FacetVolume.continuous_tail line 24
  4. lemma OAI.FacetVolume.compact_slice line 27
  5. lemma OAI.FacetVolume.sliceVolume_nonneg line 41
  6. lemma OAI.FacetVolume.slice_nonempty_of_volume_pos line 44
  7. lemma OAI.FacetVolume.weighted_cons line 50
  8. lemma OAI.FacetVolume.slices_combination_volume line 55
  9. lemma OAI.FacetVolume.log_sliceVolume_concave line 68
  10. lemma OAI.FacetVolume.continuousOn_sliceVolume line 84
  11. lemma OAI.FacetVolume.integral_indicator_one line 93
  12. lemma OAI.FacetVolume.integrable_indicator_pair line 98
  13. lemma OAI.FacetVolume.sliceVolume_as_integral line 113
  14. lemma OAI.FacetVolume.integrable_sliceVolume line 124
  15. lemma OAI.FacetVolume.integral_sliceVolume line 129