OAI/Probability/SKValue/Equations/LipschitzCompMemLpFinite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.lipschitz_comp_memLp_finite line 28
2. lemma OAI.SKValue.coupled_euler_memLp line 40
3. lemma OAI.SKValue.coupled_lipschitz_expectation_bound line 53
4. lemma OAI.SKValue.perturbed_monotone_weighted_grid_tendsto line 90
5. lemma OAI.SKValue.ValueStrip.product_lipschitzWith line 138
6. lemma OAI.SKValue.valueMeshEnergy_expectation line 146
7. theorem OAI.SKValue.diffusion_value_expectation line 180