OAI/Probability/SKValue/Processes/MeshBrownian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.coupled_terminal_second_moment_bound line 28
2. theorem OAI.SKValue.diffusion_gradient_isometry line 71
3. lemma OAI.SKValue.weighted_first_moment_perturbation line 132
4. lemma OAI.SKValue.brownian_eval_second_moment line 157
5. def OAI.SKValue.meshBrownian line 164
6. lemma OAI.SKValue.meshBrownian_measurable line 167
7. lemma OAI.SKValue.meshBrownian_memLp line 172
8. lemma OAI.SKValue.coupled_meshBrownian line 179
9. lemma OAI.SKValue.meshBrownian_second_moment line 190
10. lemma OAI.SKValue.mesh_terminal_brownian_error line 203
11. lemma OAI.SKValue.coupled_terminal_brownian_error line 228
12. theorem OAI.SKValue.diffusion_gradient_brownian_covariance line 277