OAI/Probability/Ballisticity/Stationary/ArrayDust.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.arrayDust line 15
  2. lemma OAI.DirectionalTransience.arrayDust_measurable line 18
  3. def OAI.DirectionalTransience.arrayDustFrequency line 23
  4. lemma OAI.DirectionalTransience.currentDust_array line 26
  5. lemma OAI.DirectionalTransience.currentDustFrequency_array line 29
  6. lemma OAI.DirectionalTransience.arrayDustFrequency_nonneg line 32
  7. lemma OAI.DirectionalTransience.arrayDust_current_isolated line 37
  8. lemma OAI.DirectionalTransience.arraySurvivalAverage_le_one line 50
  9. lemma OAI.DirectionalTransience.arrayDustWeight_le_survival line 62
  10. lemma OAI.DirectionalTransience.array_dust_reference_facts line 79
  11. lemma OAI.DirectionalTransience.array_dust_frequency_zero line 115
  12. lemma OAI.DirectionalTransience.arrayDust_perm line 152
  13. lemma OAI.DirectionalTransience.array_no_dust_on_frequency_zero line 155
  14. lemma OAI.DirectionalTransience.array_no_dust_on_cost_decay line 186