OAI/Probability/LogConcave/Sampling/NormalizedDirection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.stdGaussian_orthogonalProjection line 20
2. theorem OAI.LogConcaveSampling.ae_stdGaussian_ne_zero_of_unit line 35
3. def OAI.LogConcaveSampling.normalizedDirection line 52
4. theorem OAI.LogConcaveSampling.measurable_normalizedDirection line 54
5. theorem OAI.LogConcaveSampling.norm_normalizedDirection line 60
6. lemma OAI.LogConcaveSampling.normalizedDirection_scale line 68