OAI/Probability/SKBarriers/Parisi/QuantileTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.unitCDF line 16
2. theorem OAI.SK.Analytic.unitCDF_indicator line 18
3. theorem OAI.SK.Analytic.unitCDF_integrable line 22
4. theorem OAI.SK.Analytic.unitCDF_integral line 26
5. theorem OAI.SK.Analytic.unitCDF_distance_integral line 38
6. theorem OAI.SK.Analytic.unitCDF_sum_abs line 56
7. theorem OAI.SK.Analytic.quantileCDF_eq_unitCDF_sum line 89
8. theorem OAI.SK.Analytic.quantileCDF_L1_eq line 97
9. theorem OAI.SK.Analytic.atomicParisi_lipschitz_cdf line 113