OAI/Probability/Renewal/Tilt.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HoneycombLocal.tilt line 10
2. lemma OAI.HoneycombLocal.tilt_toMeasure line 14
3. lemma OAI.HoneycombLocal.tilt_apply line 19
4. lemma OAI.HoneycombLocal.tilt_apply_real line 26
5. lemma OAI.HoneycombLocal.integral_tilt line 30
6. lemma OAI.HoneycombLocal.integrable_tilt_iff line 39
7. lemma OAI.HoneycombLocal.measureReal_tilt line 46
8. lemma OAI.HoneycombLocal.measureReal_tilt_lower line 53
9. lemma OAI.HoneycombLocal.tilt_char_difference line 71