OAI/Probability/LogConcave/OraclePrograms/DampingCoefficient.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.SeedAbsorption.dual_comp_norm line 18
2. theorem OAI.LogConcaveSampling.SeedAbsorption.restore_gaussian line 27
3. theorem OAI.LogConcaveSampling.SeedAbsorption.absorb_center_noise line 56
4. def OAI.LogConcaveSampling.SeedAbsorption.dampingCoefficient line 91
5. def OAI.LogConcaveSampling.SeedAbsorption.seedDamping line 93
6. lemma OAI.LogConcaveSampling.SeedAbsorption.dampingCoefficient_identity line 96
7. lemma OAI.LogConcaveSampling.SeedAbsorption.seedDamping_adjoint line 104
8. lemma OAI.LogConcaveSampling.SeedAbsorption.seedDamping_covariance line 110
9. lemma OAI.LogConcaveSampling.SeedAbsorption.seedDamping_positive line 125
10. theorem OAI.LogConcaveSampling.SeedAbsorption.seedDamping_restore line 144
11. theorem OAI.LogConcaveSampling.SeedAbsorption.restore_gaussian_with_anchor line 168
12. theorem OAI.LogConcaveSampling.SeedAbsorption.absorb_center_noise_with_anchor line 178
13. theorem OAI.LogConcaveSampling.SeedAbsorption.restore_gaussian_blocks line 217
14. theorem OAI.LogConcaveSampling.SeedAbsorption.restore_gaussian_blocks_with_anchor line 225
15. theorem OAI.LogConcaveSampling.SeedAbsorption.absorb_center_noise_blocks line 236