OAI/Probability/Ballisticity/Estimates/TailProfile.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TailSampling.measurable_profile_cuts line 15
  2. def OAI.TailSampling.lowerKernel line 48
  3. def OAI.TailSampling.upperKernel line 52
  4. lemma OAI.TailSampling.lowerKernel_markov line 56
  5. lemma OAI.TailSampling.upperKernel_markov line 68
  6. lemma OAI.TailSampling.lowerKernel_supported line 81
  7. lemma OAI.TailSampling.upperKernel_supported line 88
  8. abbrev OAI.DirectionalTransience.ZeroHeightPair line 104
  9. def OAI.DirectionalTransience.horizontalPair line 107
  10. def OAI.DirectionalTransience.profilePairKernel line 113
  11. lemma OAI.DirectionalTransience.profilePairKernel_markov line 120
  12. lemma OAI.DirectionalTransience.profilePairKernel_supported line 131
  13. lemma OAI.DirectionalTransience.profilePairKernel_integral line 150
  14. lemma OAI.DirectionalTransience.profilePairKernel_integrable line 166