OAI/Probability/LogConcave/Sampling/MeanMaterialL2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.mean_material_l2 line 15
2. lemma OAI.LogConcaveSampling.joint_material_direction line 53
3. lemma OAI.LogConcaveSampling.fullProbabilityFlow_deriv line 73
4. lemma OAI.LogConcaveSampling.material_path_chain line 84
5. lemma OAI.LogConcaveSampling.mean_material_path_deriv line 95
6. lemma OAI.LogConcaveSampling.fullProbabilityFlow_interpolation line 106
7. lemma OAI.LogConcaveSampling.interpolationLaw_initial line 118
8. lemma OAI.LogConcaveSampling.fullProbabilityFlow_initial line 126
9. lemma OAI.LogConcaveSampling.fullProbabilityFlow_interpolation_closed line 132
10. lemma OAI.LogConcaveSampling.JetCalculus.TimeSmooth.slice_continuous line 141
11. lemma OAI.LogConcaveSampling.mean_material_path_energy line 148