OAI/Probability/Ballisticity/Coupling/QuenchedMoments.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.noDropQuenchedKernel line 15
  2. lemma OAI.DirectionalTransience.noDropQuenchedKernel_apply line 25
  3. lemma OAI.DirectionalTransience.noDropQuenched_le_one line 31
  4. lemma OAI.DirectionalTransience.noDropQuenched_ne_top line 34
  5. instance OAI.DirectionalTransience.noDropQuenchedKernel_finite line 37
  6. lemma OAI.DirectionalTransience.noDropQuenchedKernel_probability line 45
  7. def OAI.DirectionalTransience.quenchedNoDropTest line 52
  8. lemma OAI.DirectionalTransience.measurable_quenchedNoDropTest line 56
  9. lemma OAI.DirectionalTransience.noDrop_mass_smul_kernel line 60
  10. lemma OAI.DirectionalTransience.noDrop_pair_mass_smul_kernel line 70
  11. def OAI.DirectionalTransience.noDropPairEnvironment line 85
  12. lemma OAI.DirectionalTransience.noDropPairEnvironment_probability line 90
  13. lemma OAI.DirectionalTransience.noDrop_pair_disintegration line 99
  14. lemma OAI.DirectionalTransience.noDropPairEnvironment_ae_positive line 123
  15. lemma OAI.DirectionalTransience.integral_kernel_average line 132
  16. lemma OAI.DirectionalTransience.noDrop_pair_test_moment line 139
  17. lemma OAI.DirectionalTransience.noDrop_pair_test_first_moment line 163
  18. lemma OAI.DirectionalTransience.noDrop_pair_test_second_moment line 177
  19. def OAI.DirectionalTransience.medianFirstHitPath line 184
  20. lemma OAI.DirectionalTransience.measurable_medianFirstHitPath line 190
  21. def OAI.DirectionalTransience.quenchedMedianPathTest line 198
  22. lemma OAI.DirectionalTransience.measurable_quenchedMedianPathTest line 203
  23. lemma OAI.DirectionalTransience.quenchedMedianPathTest_moments line 210