OAI/Probability/LatticeSurface/Convexity/WeightedPrekopa.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FacetVolume.weighted_transport_amgm line 15
2. lemma OAI.FacetVolume.weighted_quantile_substitution line 30
3. lemma OAI.FacetVolume.weighted_quantile_integral_lower line 56
4. theorem OAI.FacetVolume.interval_weighted_prekopa_leindler line 92