OAI/Probability/LatticeSurface/Convexity/QuantileTransport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FacetVolume.cumulative line 13
  2. def OAI.FacetVolume.quantile line 16
  3. lemma OAI.FacetVolume.integral_positive line 19
  4. lemma OAI.FacetVolume.cumulative_hasDerivAt line 23
  5. lemma OAI.FacetVolume.continuous_cumulative line 28
  6. lemma OAI.FacetVolume.cumulative_strictMonoOn line 32
  7. lemma OAI.FacetVolume.cumulative_left line 41
  8. lemma OAI.FacetVolume.cumulative_right line 44
  9. lemma OAI.FacetVolume.cumulative_surjOn line 48
  10. lemma OAI.FacetVolume.quantile_mem line 55
  11. lemma OAI.FacetVolume.cumulative_quantile line 60
  12. lemma OAI.FacetVolume.quantile_cumulative line 65
  13. lemma OAI.FacetVolume.quantile_left line 70
  14. lemma OAI.FacetVolume.quantile_right line 75
  15. lemma OAI.FacetVolume.quantile_strictMonoOn line 80
  16. lemma OAI.FacetVolume.quantile_mem_Ioo line 88
  17. lemma OAI.FacetVolume.quantile_image_Ioo line 98
  18. lemma OAI.FacetVolume.quantile_continuousAt line 113
  19. lemma OAI.FacetVolume.quantile_hasDerivAt line 121