OAI/Computability/PerfectCompleteness/Sampling/DensityVariation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.DensityVariation.expectation_sub line 20
2. theorem OAI.PerfectCompleteness.DensityVariation.expectation_mul_const line 24
3. theorem OAI.PerfectCompleteness.DensityVariation.expectation_div line 28
4. def OAI.PerfectCompleteness.DensityVariation.reweight line 32
5. theorem OAI.PerfectCompleteness.DensityVariation.variation_eq_density line 39
6. theorem OAI.PerfectCompleteness.DensityVariation.variation_le_sqrt line 50
7. theorem OAI.PerfectCompleteness.DensityVariation.variation_pushforward_le line 63
8. theorem OAI.PerfectCompleteness.DensityVariation.observed_variation_le_sqrt line 90