OAI/Probability/Ballisticity/Crossings/FirstHitUpward.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.single_step_dirac_le_hitKernel line 14
2. lemma OAI.DirectionalTransience.elliptic_single_step_le_hitKernel line 40
3. lemma OAI.DirectionalTransience.hitKernel_direct_step_retention line 49
4. lemma OAI.DirectionalTransience.coordinate_hitKernel_supported line 76
5. lemma OAI.DirectionalTransience.coordinate_hitKernel_upward_retention line 90