OAI/Geometry/CAT0Fillings/Transport/RadialCDF.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CAT0Fillings.RadialSobolev.cumulativeOrderIso line 13
  2. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeOrderIso_apply line 26
  3. def OAI.CAT0Fillings.RadialSobolev.cumulativeInverse line 30
  4. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeInverse_mem line 35
  5. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeInverse_continuous line 39
  6. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeInverse_right line 44
  7. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeInverse_left line 52
  8. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeInverse_interior line 59
  9. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeInverse_hasDerivAt line 72
  10. lemma OAI.CAT0Fillings.RadialSobolev.cumulativeTransport_hasDerivAt line 81
  11. def OAI.CAT0Fillings.RadialSobolev.radialCDF line 99
  12. lemma OAI.CAT0Fillings.RadialSobolev.radialCDF_hasDerivAt line 102
  13. lemma OAI.CAT0Fillings.RadialSobolev.radialCDF_continuous line 113
  14. lemma OAI.CAT0Fillings.RadialSobolev.radialCDF_zero line 117
  15. lemma OAI.CAT0Fillings.RadialSobolev.radialCDF_strictMonoOn line 120
  16. def OAI.CAT0Fillings.RadialSobolev.radialTransport line 131
  17. lemma OAI.CAT0Fillings.RadialSobolev.radialTransport_mem line 137
  18. lemma OAI.CAT0Fillings.RadialSobolev.radialTransport_continuous line 143
  19. lemma OAI.CAT0Fillings.RadialSobolev.radialTransport_cdf line 149
  20. lemma OAI.CAT0Fillings.RadialSobolev.radialTransport_interior line 162
  21. lemma OAI.CAT0Fillings.RadialSobolev.radialTransport_hasDerivAt line 175