OAI/Probability/LogConcave/Sampling/IdentityOutputEmbedding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.identityOutputEmbedding line 16
2. def OAI.LogConcaveSampling.identityOutputProjection line 19
3. lemma OAI.LogConcaveSampling.identityOutputProjection_vector line 22
4. lemma OAI.LogConcaveSampling.identityOutputProjection_lie line 28
5. lemma OAI.LogConcaveSampling.projection_chainTaylor line 44
6. lemma OAI.LogConcaveSampling.projection_rms line 50