OAI/Probability/Ballisticity/Walk/FixedQuenchedKernel.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.conditioned_word_spatial_strong_laws line 12
  2. lemma OAI.DirectionalTransience.increasing_cuts_index_tendsto line 32
  3. lemma OAI.DirectionalTransience.scalar_cut_interpolation line 41
  4. lemma OAI.DirectionalTransience.regeneration_coordinate_sum line 60
  5. lemma OAI.DirectionalTransience.conditioned_coordinate_transience line 70
  6. lemma OAI.DirectionalTransience.conditioned_to_annealed_transience line 92
  7. lemma OAI.DirectionalTransience.dot_comm line 150
  8. lemma OAI.DirectionalTransience.dot_signed_direction line 153
  9. lemma OAI.DirectionalTransience.signed_direction_unit line 158
  10. lemma OAI.DirectionalTransience.exists_transient_signed_coordinate line 164
  11. def OAI.DirectionalTransience.fixedQuenchedKernel line 173
  12. instance OAI.DirectionalTransience.fixedQuenchedKernel_markov line 177
  13. def OAI.DirectionalTransience.sharedPairKernel line 180
  14. instance OAI.DirectionalTransience.sharedPairKernel_markov line 184
  15. def OAI.DirectionalTransience.sharedPairLaw line 187
  16. instance OAI.DirectionalTransience.sharedPairLaw_probability line 190
  17. def OAI.DirectionalTransience.sharedNoDropMass line 195
  18. lemma OAI.DirectionalTransience.sharedPairLaw_rectangle line 199
  19. lemma OAI.DirectionalTransience.sharedNoDropMass_eq line 209
  20. lemma OAI.DirectionalTransience.sharedNoDropMass_le_one line 213
  21. lemma OAI.DirectionalTransience.sharedNoDropMass_uniform_positive line 218
  22. def OAI.DirectionalTransience.sharedConditionedPairLaw line 272
  23. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_probability line 277
  24. def OAI.DirectionalTransience.annealedFrom line 285
  25. instance OAI.DirectionalTransience.annealedFrom_probability line 288
  26. lemma OAI.DirectionalTransience.annealedFrom_apply line 293
  27. lemma OAI.DirectionalTransience.annealedFrom_noDrop line 299
  28. def OAI.DirectionalTransience.conditionedFrom line 305
  29. lemma OAI.DirectionalTransience.conditionedFrom_probability line 309
  30. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_fst_le line 317
  31. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_snd_le line 339
  32. lemma OAI.DirectionalTransience.shared_pair_word_suffix line 362
  33. lemma OAI.DirectionalTransience.noDrop_real_integral_translation line 407