OAI/Probability/LatticeSurface/Convexity/QuantitativeTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SliceTransport.amgm_ratio_ge_one line 16
2. lemma OAI.SliceTransport.amgm_ratio_quantitative line 23
3. lemma OAI.SliceTransport.midpoint_quantile_substitution line 54
4. lemma OAI.SliceTransport.transport_amgm_quantitative line 79
5. lemma OAI.SliceTransport.integral_sq_ge_sq_integral line 103
6. lemma OAI.SliceTransport.integral_difference_velocity_sq line 117
7. lemma OAI.SliceTransport.quantitative_integrand_integrable line 137
8. lemma OAI.SliceTransport.midpoint_quantile_defect_lower line 146