OAI/Probability/ThreeState/Supercritical.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Boundary score moments and reconstruction above the Kesten–Stigum threshold.

  1. def OAI.ThreeState.listScore line 10
  2. def OAI.ThreeState.multisetScore line 11
  3. lemma OAI.ThreeState.listScore_cons line 13
  4. lemma OAI.ThreeState.multisetScore_coe line 16
  5. lemma OAI.ThreeState.iidList_moments line 20
  6. lemma OAI.ThreeState.iidMultiset_moments line 34
  7. lemma OAI.ThreeState.compound_moments line 43
  8. def OAI.ThreeState.spinScore line 60
  9. def OAI.ThreeState.boundaryScore line 62
  10. lemma OAI.ThreeState.mass_channel line 66
  11. lemma OAI.ThreeState.channel_score line 70
  12. def OAI.ThreeState.scoreSecond line 76
  13. theorem OAI.ThreeState.boundaryScore_moments line 82
  14. lemma OAI.ThreeState.hasMean_marginal line 104
  15. lemma OAI.ThreeState.mean_uniform line 108
  16. lemma OAI.ThreeState.mean_marginal line 113
  17. lemma OAI.ThreeState.mean_uniform_spinScore line 118
  18. lemma OAI.ThreeState.mean_uniform_spinScore_square line 121
  19. lemma OAI.ThreeState.mean_uniform_channel line 124
  20. lemma OAI.ThreeState.pow_square_comm line 129
  21. lemma OAI.ThreeState.scoreSecond_average_zero line 132
  22. lemma OAI.ThreeState.scoreSecond_average_succ line 135
  23. lemma OAI.ThreeState.scoreSecond_bound line 151
  24. lemma OAI.ThreeState.boundaryScore_marginal_moments line 162
  25. lemma OAI.ThreeState.HasMean.mul_of_square line 174
  26. lemma OAI.ThreeState.mean_cauchy_square line 184
  27. lemma OAI.ThreeState.posterior_le_one line 205
  28. def OAI.ThreeState.posteriorTV line 211
  29. lemma OAI.ThreeState.posteriorTV_nonneg line 214
  30. lemma OAI.ThreeState.posteriorTV_le_two line 218
  31. lemma OAI.ThreeState.hasMean_posteriorTV line 228
  32. lemma OAI.ThreeState.mean_posteriorTV line 232
  33. def OAI.ThreeState.posteriorScore line 235
  34. lemma OAI.ThreeState.posteriorScore_square_le line 238
  35. lemma OAI.ThreeState.hasMean_posteriorScore_square line 255
  36. lemma OAI.ThreeState.mean_posteriorScore_square_le line 260
  37. lemma OAI.ThreeState.weighted_posteriorScore line 266
  38. lemma OAI.ThreeState.mean_score_correlation line 272
  39. theorem OAI.ThreeState.advantage_lower_from_score line 284
  40. lemma OAI.ThreeState.supercritical_advantage_bound line 299
  41. theorem OAI.ThreeState.reconstructs_supercritical_of_moments line 329
  42. theorem OAI.ThreeState.regular_supercritical line 354

    Distinct definitions of this name: ComparatorChallenges/ThreeStateSupercritical.lean:98 (different declaration text). Qualify references as OAI.ThreeState.regular_supercritical@path.

  43. theorem OAI.ThreeState.poisson_supercritical line 366

    Distinct definitions of this name: ComparatorChallenges/ThreeStateSupercritical.lean:102 (different declaration text). Qualify references as OAI.ThreeState.poisson_supercritical@path.