OAI/Probability/LogConcave/Sampling/InterpolationResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.integrable_lipschitz_comp_of_integrable line 20
2. lemma OAI.LogConcaveSampling.primitive_identity_integrable line 33
3. def OAI.LogConcaveSampling.interpolationResidual line 42
4. lemma OAI.LogConcaveSampling.interpolationResidual_integrable line 46
5. lemma OAI.LogConcaveSampling.conditional_residual_zero line 70
6. lemma OAI.LogConcaveSampling.integrable_scaled_affine_const line 87
7. lemma OAI.LogConcaveSampling.conditional_residual_integrable line 92
8. theorem OAI.LogConcaveSampling.interpolation_flux_zero line 101