OAI/Probability/Ballisticity/Estimates/IndependentDyadic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.independent_dyadic_centered line 14
  2. lemma OAI.DirectionalTransience.ReferenceClasses.representative_singleton line 52
  3. lemma OAI.DirectionalTransience.ReferenceClasses.displacement_singleton line 56
  4. def OAI.DirectionalTransience.ReferenceClasses.dustFrequency line 62
  5. def OAI.DirectionalTransience.ReferenceClasses.dustWeight line 65
  6. lemma OAI.DirectionalTransience.ReferenceClasses.dustWeight_measurable line 72
  7. lemma OAI.DirectionalTransience.ReferenceClasses.reference_dust_dyadic line 86
  8. def OAI.DirectionalTransience.upperNoDrop line 153
  9. lemma OAI.DirectionalTransience.upperNoDrop_measurable line 156
  10. lemma OAI.DirectionalTransience.upperNoDrop_le_one line 159
  11. lemma OAI.DirectionalTransience.upperEnvironment_restrict_eq line 161
  12. lemma OAI.DirectionalTransience.upperNoDrop_restrict line 167
  13. lemma OAI.DirectionalTransience.upperKernel_restrict line 175
  14. lemma OAI.DirectionalTransience.upperNoDrop_le_kernel_ae line 188
  15. lemma OAI.DirectionalTransience.upperNoDrop_positive_ae line 207
  16. lemma OAI.DirectionalTransience.upperNoDrop_inverse_moment line 218