OAI/Probability/LatticeSurface/Convexity/InteriorQuantile.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SliceTransport.cumulative line 13
  2. def OAI.SliceTransport.quantile line 16
  3. structure OAI.SliceTransport.IntervalDensity line 19
  4. lemma OAI.SliceTransport.IntervalDensity.continuousAt line 23
  5. lemma OAI.SliceTransport.integral_positive line 27
  6. lemma OAI.SliceTransport.cumulative_hasDerivAt line 31
  7. lemma OAI.SliceTransport.continuousOn_cumulative line 41
  8. lemma OAI.SliceTransport.cumulative_strictMonoOn line 47
  9. lemma OAI.SliceTransport.cumulative_left line 56
  10. lemma OAI.SliceTransport.cumulative_right line 59
  11. lemma OAI.SliceTransport.cumulative_surjOn line 63
  12. lemma OAI.SliceTransport.quantile_mem line 70
  13. lemma OAI.SliceTransport.cumulative_quantile line 75
  14. lemma OAI.SliceTransport.quantile_cumulative line 80
  15. lemma OAI.SliceTransport.quantile_left line 85
  16. lemma OAI.SliceTransport.quantile_right line 90
  17. lemma OAI.SliceTransport.quantile_strictMonoOn line 95
  18. lemma OAI.SliceTransport.quantile_mem_Ioo line 103
  19. lemma OAI.SliceTransport.quantile_image_Ioo line 113
  20. lemma OAI.SliceTransport.quantile_continuousAt line 128
  21. lemma OAI.SliceTransport.quantile_hasDerivAt line 136
  22. lemma OAI.SliceTransport.cumulative_mem line 148
  23. lemma OAI.SliceTransport.quantile_continuousOn line 156