OAI/Probability/LogConcave/Analysis/GaussianAffineNormMoment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.gaussian_affine_norm_moment line 14
2. lemma OAI.LogConcaveSampling.gaussian_growth_sq_moment line 32
3. lemma OAI.LogConcaveSampling.conditionalFieldMean_at_zero line 49
4. lemma OAI.LogConcaveSampling.terminal_mean_error line 61
5. theorem OAI.LogConcaveSampling.terminal_mean_squared_error line 77
6. theorem OAI.LogConcaveSampling.terminal_sample_squared_error line 88
7. lemma OAI.LogConcaveSampling.gaussian_lipschitz_memLp line 115
8. lemma OAI.LogConcaveSampling.gaussian_scaled_growth_sq_moment line 125
9. lemma OAI.LogConcaveSampling.probabilityFlow_initial_displacement line 154
10. lemma OAI.LogConcaveSampling.probabilityFlow_initial_rms line 207