OAI/Probability/Ballisticity/Estimates/Sampling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.finiteOffsetTest line 13
  2. lemma OAI.DirectionalTransience.finiteOffsetTest_continuous line 16
  3. def OAI.DirectionalTransience.arrayOffsetTest line 32
  4. def OAI.DirectionalTransience.arrayProfileTest line 37
  5. def OAI.DirectionalTransience.arraySamplingError line 41
  6. lemma OAI.DirectionalTransience.arrayOffsetTest_mem line 46
  7. lemma OAI.DirectionalTransience.arrayProfileTest_mem line 51
  8. lemma OAI.DirectionalTransience.arraySamplingError_bound line 54
  9. lemma OAI.DirectionalTransience.actual_array_error_atom line 74
  10. lemma OAI.DirectionalTransience.actual_array_sampling_sq_conditional line 102
  11. lemma OAI.DirectionalTransience.actual_array_offset line 123
  12. lemma OAI.DirectionalTransience.actual_array_profile line 138
  13. lemma OAI.DirectionalTransience.actual_array_sampling_test_conditional line 144