OAI/Probability/SKRatio/Dynamics/StepMass.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKRatioClock.Clock.scheffe_density line 14
2. theorem OAI.SKRatioClock.Clock.scheffe_density_filter line 51
3. def OAI.SKRatioClock.Clock.stepMass line 89
4. lemma OAI.SKRatioClock.Clock.stepMass_of_nonneg line 92
5. lemma OAI.SKRatioClock.Clock.stepMass_of_neg line 103
6. lemma OAI.SKRatioClock.Clock.stepMass_nonneg line 114
7. lemma OAI.SKRatioClock.Clock.integral_step_interval line 120
8. lemma OAI.SKRatioClock.Clock.integrable_step_interval line 125
9. lemma OAI.SKRatioClock.Clock.integral_step_interval_norm line 130
10. lemma OAI.SKRatioClock.Clock.integral_stepMass line 139
11. lemma OAI.SKRatioClock.Clock.integrable_stepMass line 146
12. def OAI.SKRatioClock.Clock.histogram line 151
13. lemma OAI.SKRatioClock.Clock.integrable_histogram line 154
14. lemma OAI.SKRatioClock.Clock.integral_histogram line 162
15. lemma OAI.SKRatioClock.Clock.histogram_nonneg line 177