OAI/Probability/Ballisticity/Crossings/FirstLayerHitConcat.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.firstLayerHit_concat line 249
2. lemma OAI.DirectionalTransience.stayUntil_concat line 262
3. lemma OAI.DirectionalTransience.futureNoDrop_concat line 276
4. lemma OAI.DirectionalTransience.layerPairPrefix_truth_concat line 281
5. lemma OAI.DirectionalTransience.measurableSet_layerPairTruthEvent line 303
6. lemma OAI.DirectionalTransience.shared_layer_restart_lower line 309