OAI/Probability/LogConcave/Sampling/HarmonicPositionDeriv.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.harmonic_position_deriv line 13
2. theorem OAI.LogConcaveSampling.kernel_action_derivative line 28
3. lemma OAI.LogConcaveSampling.meanOutputProjection_correction line 75
4. lemma OAI.LogConcaveSampling.projection_derivativeStencil line 86
5. lemma OAI.LogConcaveSampling.kernel_action_lie_projection line 92
6. theorem OAI.LogConcaveSampling.kernel_action_stencil_rms line 123