OAI/Probability/LogConcave/Sampling/Correlation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.centerScaleRate line 12
2. lemma OAI.LogConcaveSampling.centerStateQuadratureEnvelope_rate line 17
3. lemma OAI.LogConcaveSampling.centerInitialEnvelope_rate line 25
4. lemma OAI.LogConcaveSampling.centerStateEnvelope_rate line 29
5. lemma OAI.LogConcaveSampling.centerMeanEnvelope_rate line 47
6. theorem OAI.LogConcaveSampling.centeringEnvelopes_calibrated line 65
7. def OAI.LogConcaveSampling.sourceCorrelation line 105
8. lemma OAI.LogConcaveSampling.sourceCorrelation_eventually line 107
9. lemma OAI.LogConcaveSampling.sourceCorrelation_tendsto line 124
10. lemma OAI.LogConcaveSampling.sourceMesh_eventually line 131
11. lemma OAI.LogConcaveSampling.sourceAngle_eventually line 147
12. lemma OAI.LogConcaveSampling.probabilityMeanLipschitz_rate line 167
13. theorem OAI.LogConcaveSampling.centeringScalarCalibration line 177