OAI/Probability/Ballisticity/Geometry/LatticeVector.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.stationary_initial_average_truncated_bound line 12
  2. lemma OAI.DirectionalTransience.truncatedMean_ratio_tendsto_zero line 54
  3. lemma OAI.DirectionalTransience.real_integrable_of_scaled_truncation_bound line 75
  4. lemma OAI.DirectionalTransience.exists_minimal_truncation_scale line 104
  5. lemma OAI.DirectionalTransience.minimal_truncation_scale_upper line 129
  6. def OAI.DirectionalTransience.latticeVector line 144
  7. lemma OAI.DirectionalTransience.latticeVector_zero line 147
  8. lemma OAI.DirectionalTransience.latticeVector_add line 151
  9. lemma OAI.DirectionalTransience.latticeVector_sub line 156
  10. lemma OAI.DirectionalTransience.latticeVector_step_norm line 161
  11. def OAI.DirectionalTransience.wordRadius line 169
  12. lemma OAI.DirectionalTransience.wordRadius_bound line 174
  13. lemma OAI.DirectionalTransience.wordRadius_nonneg line 180
  14. lemma OAI.DirectionalTransience.wordRadius_attained line 184
  15. lemma OAI.DirectionalTransience.wordRadius_le_length line 191
  16. lemma OAI.DirectionalTransience.measurable_wordRadius line 205
  17. lemma OAI.DirectionalTransience.conditioned_radius_initial_average_bound line 207
  18. lemma OAI.DirectionalTransience.affine_envelope_of_average_limit line 220
  19. lemma OAI.DirectionalTransience.uniform_affine_envelope_probability line 246
  20. lemma OAI.DirectionalTransience.conditioned_height_template line 275
  21. lemma OAI.DirectionalTransience.truncation_threshold_eventually_large line 298
  22. lemma OAI.DirectionalTransience.truncated_template_failure_bound line 315
  23. lemma OAI.DirectionalTransience.restricted_union_lower_bound line 335
  24. lemma OAI.DirectionalTransience.independent_rare_words_lower_bound line 365
  25. lemma OAI.DirectionalTransience.annealed_avoiding_suffix line 386