OAI/Probability/SKValue/Equations/ForwardDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKValue.ForwardDensityData line 13
2. def OAI.SKValue.ForwardDensityData.weight line 24
3. def OAI.SKValue.ForwardDensityData.jet line 26
4. lemma OAI.SKValue.ForwardDensityData.weight_pos line 29
5. lemma OAI.SKValue.ForwardDensityData.weight_measurable line 31
6. lemma OAI.SKValue.ForwardDensityData.jet_initial line 33
7. lemma OAI.SKValue.ForwardDensityData.jet_space line 39
8. lemma OAI.SKValue.ForwardDensityData.jet_continuous line 43
9. def OAI.SKValue.ForwardDensityData.evolve line 46
10. lemma OAI.SKValue.ForwardDensityData.evolve_weight line 59
11. lemma OAI.SKValue.ForwardDensityData.evolve_jet line 74
12. lemma OAI.SKValue.ForwardDensityData.evolve_slope_concavity line 97