OAI/Probability/Ballisticity/Coupling/GaussianQuenchedTube.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.quenched_median_test_concentration_of_law line 16
2. def OAI.DirectionalTransience.medianTubeEndpoint line 40
3. lemma OAI.DirectionalTransience.measurableSet_medianTubeEndpoint line 46
4. lemma OAI.DirectionalTransience.quenched_gaussian_noDrop_tube_from_test line 55