OAI/Probability/Ballisticity/Geometry/HeightSlab.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.convexOn_rpow_nonpos_Ici line 12
  2. lemma OAI.DirectionalTransience.inverse_jensen_bounded line 33
  3. lemma OAI.DirectionalTransience.inverse_mixture_markov line 51
  4. theorem OAI.DirectionalTransience.separated_initial_inverse_moment line 96
  5. lemma OAI.DirectionalTransience.hitKernel_apply_eq_hit line 168
  6. lemma OAI.DirectionalTransience.hit_concatenation line 175
  7. lemma OAI.DirectionalTransience.hitKernel_comp_le line 191
  8. def OAI.DirectionalTransience.HeightSlab line 202
  9. def OAI.DirectionalTransience.HeightLayer line 205
  10. lemma OAI.DirectionalTransience.heightSlab_disjoint_layer line 208
  11. def OAI.DirectionalTransience.heightKernel line 214
  12. lemma OAI.DirectionalTransience.heightKernel_total_le_one line 218
  13. instance OAI.DirectionalTransience.heightKernel_finite line 222
  14. lemma OAI.DirectionalTransience.heightKernel_supported line 226
  15. lemma OAI.DirectionalTransience.heightKernel_rows line 236
  16. lemma OAI.DirectionalTransience.heightKernel_comp_le line 242
  17. def OAI.DirectionalTransience.normalizedMeasure line 252
  18. lemma OAI.DirectionalTransience.normalizedMeasure_probability line 255
  19. lemma OAI.DirectionalTransience.mass_smul_normalizedMeasure line 262
  20. lemma OAI.DirectionalTransience.integral_normalized_comp line 271
  21. lemma OAI.DirectionalTransience.retained_kernel_comp_le line 277
  22. lemma OAI.DirectionalTransience.pathCylinder_weight_locality line 288
  23. lemma OAI.DirectionalTransience.quenched_restrict_stay_congr line 299
  24. lemma OAI.DirectionalTransience.quenched_stay_event_congr line 335
  25. lemma OAI.DirectionalTransience.measurable_quenched_stay_event_rows line 343
  26. lemma OAI.DirectionalTransience.annealed_event_translation line 352
  27. lemma OAI.DirectionalTransience.annealed_record_suffix line 369