OAI/Probability/SKRatio/Dynamics/ClockBridge.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Calculus.kernel_apply line 13
  2. def OAI.SKRatio.Calculus.attemptKernel line 20
  3. lemma OAI.SKRatio.Calculus.attemptKernel_nonneg line 23
  4. lemma OAI.SKRatio.Calculus.attemptKernel_eq_transition line 28
  5. def OAI.SKRatio.Calculus.residualAttempt line 34
  6. lemma OAI.SKRatio.Calculus.residualAttempt_apply line 38
  7. lemma OAI.SKRatio.Calculus.attempt_eq_lazy_residual line 43
  8. lemma OAI.SKRatio.Calculus.residualAttempt_const line 47
  9. lemma OAI.SKRatio.Calculus.residualAttempt_pow_const line 54
  10. lemma OAI.SKRatio.Calculus.residualAttempt_nonneg line 60
  11. lemma OAI.SKRatio.Calculus.residualAttempt_pow_nonneg line 76
  12. lemma OAI.SKRatio.Calculus.residualAttempt_pow_abs_le line 86
  13. lemma OAI.SKRatio.Calculus.residual_semigroup_uniformization line 101
  14. lemma OAI.SKRatio.Calculus.residual_poisson_hasSum line 123
  15. lemma OAI.SKRatio.Calculus.natCastCLM_apply line 137
  16. lemma OAI.SKRatio.Calculus.residual_binomial_sum line 143
  17. lemma OAI.SKRatio.Calculus.residual_binomial_hasSum line 156
  18. lemma OAI.SKRatio.Calculus.gibbsMean_abs_le_one line 166
  19. lemma OAI.SKRatio.Calculus.residual_test_bound line 178
  20. lemma OAI.SKRatio.Calculus.residual_poisson_test line 189
  21. lemma OAI.SKRatio.Calculus.residual_binomial_test line 202
  22. lemma OAI.SKRatio.Calculus.totalVariation_test_bound line 211
  23. lemma OAI.SKRatio.Calculus.continuous_test_bound line 226
  24. lemma OAI.SKRatio.Calculus.field_square_sum_le line 234
  25. lemma OAI.SKRatio.Calculus.one_sub_tanh_half line 249
  26. lemma OAI.SKRatio.Calculus.one_add_tanh_half line 256
  27. lemma OAI.SKRatio.Calculus.siteRefresh_diagonal_lower line 260
  28. lemma OAI.SKRatio.Calculus.logistic_quadratic_lower line 285
  29. lemma OAI.SKRatio.Calculus.attempted_holding_lower line 302