OAI/Probability/LogConcave/Sampling/SampleCorrelation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.samplingEnvelope_rate line 15
2. theorem OAI.LogConcaveSampling.sampleScalarCalibration_uniform line 35
3. theorem OAI.LogConcaveSampling.exists_calibrated_sample_circuit line 68
4. lemma OAI.LogConcaveSampling.probability_endpoint_divided_law line 122
5. lemma OAI.LogConcaveSampling.probability_endpoint_noisy_law line 137
6. def OAI.LogConcaveSampling.sampleCorrelation line 153
7. lemma OAI.LogConcaveSampling.sampleCorrelation_properties line 155
8. lemma OAI.LogConcaveSampling.sample_noise_variance line 177