OAI/Probability/SATComputability/DyadicMoment.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FixedClauseThreshold.Computability.poissonKillProbability_le_one line 10
  2. theorem OAI.FixedClauseThreshold.Computability.positive_killing_in_dyadic_bin line 17
  3. def OAI.FixedClauseThreshold.Computability.dyadicLifetimeBound line 31
  4. theorem OAI.FixedClauseThreshold.Computability.dyadicLifetimeBound_nonneg line 34
  5. theorem OAI.FixedClauseThreshold.Computability.dyadic_lifetime_bound line 38
  6. theorem OAI.FixedClauseThreshold.Computability.capped_lifetime_fractional_bound line 51
  7. theorem OAI.FixedClauseThreshold.Computability.dyadicLevel_rpow line 60
  8. theorem OAI.FixedClauseThreshold.Computability.dyadicBlock_growth line 63
  9. def OAI.FixedClauseThreshold.Computability.dyadicMomentCoefficient line 78
  10. theorem OAI.FixedClauseThreshold.Computability.dyadicMomentCoefficient_nonneg line 81
  11. theorem OAI.FixedClauseThreshold.Computability.dyadicMomentCoefficient_bound line 85
  12. theorem OAI.FixedClauseThreshold.Computability.dyadicMomentCoefficient_summable line 140