OAI/Probability/LogConcave/Sampling/KernelTransportAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.kernelTransportAction line 16
2. lemma OAI.LogConcaveSampling.kernel_action_between_derivative line 20
3. lemma OAI.LogConcaveSampling.kernel_between_lie_projection line 41
4. theorem OAI.LogConcaveSampling.kernel_action_between_stencil_rms line 70
5. lemma OAI.LogConcaveSampling.finite_weighted_lipschitz line 144
6. def OAI.LogConcaveSampling.kernelActionPicard line 159
7. theorem OAI.LogConcaveSampling.kernelActionPicard_lipschitz line 168