OAI/Probability/Ballisticity/Crossings/GaussianBadCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectionalTransience.gaussian_bad_cutoff line 269
2. lemma OAI.DirectionalTransience.clippedThreeHalves_uniformContinuous line 330
3. lemma OAI.DirectionalTransience.bounded_test_perturbation line 343
4. def OAI.DirectionalTransience.physicalFirstHitGap line 384
5. lemma OAI.DirectionalTransience.measurable_physicalFirstHitGap line 389
6. lemma OAI.DirectionalTransience.measurable_nat_apply line 393
7. lemma OAI.DirectionalTransience.measurable_physicalFirstHitGap_random line 400
8. theorem OAI.DirectionalTransience.shared_observed_gap_test_transfer line 406