OAI/Probability/SKRatio/Dynamics/Median.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Calculus.continuousKernel_zero line 13
  2. lemma OAI.SKRatio.Calculus.continuousDistance_zero line 18
  3. lemma OAI.SKRatio.Calculus.continuousKernel_continuous_time line 22
  4. lemma OAI.SKRatio.Calculus.continuousDistance_continuous_time line 27
  5. lemma OAI.SKRatio.Calculus.continuousKernel_pos line 40
  6. lemma OAI.SKRatio.Calculus.continuousKernel_nat line 59
  7. lemma OAI.SKRatio.Calculus.exists_continuous_geometric_bound line 66
  8. lemma OAI.SKRatio.Calculus.exists_continuous_mixing_time line 80
  9. def OAI.SKRatio.Calculus.medianTime line 87
  10. lemma OAI.SKRatio.Calculus.medianTime_mem line 90
  11. lemma OAI.SKRatio.Calculus.medianTime_le_iff line 98
  12. lemma OAI.SKRatio.Calculus.before_median line 106
  13. lemma OAI.SKRatio.Calculus.medianTime_pos line 110
  14. lemma OAI.SKRatio.Calculus.continuousDistance_median line 121
  15. lemma OAI.SKRatio.Calculus.median_cutoff_sides_of_lag line 136
  16. lemma OAI.SKRatio.Calculus.uniform_continuous_cutoff_of_positive_lag line 176