OAI/Probability/Ballisticity/Estimates/ObservedBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectionalTransience.observedAdvance_total_charge line 15
2. def OAI.DirectionalTransience.SmallCommonLayer line 96
3. lemma OAI.DirectionalTransience.measurableSet_smallCommonLayer line 104
4. lemma OAI.DirectionalTransience.firstLayerHit_suffix_iff_of_record line 121
5. lemma OAI.DirectionalTransience.firstLayerHit_time_ge_record line 140
6. lemma OAI.DirectionalTransience.futureNoDrop_suffix_iff line 150
7. lemma OAI.DirectionalTransience.smallCommonLayer_suffix_iff line 154
8. lemma OAI.DirectionalTransience.firstLayerHit_recordIndexPosition_all line 181
9. lemma OAI.DirectionalTransience.physicalFirstHitGap_at_common line 198
10. lemma OAI.DirectionalTransience.smallCommonLayer_iff_physical line 213