OAI/Probability/ThreeState/Basic.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Three-state symmetric broadcast experiments, posterior advantage and total variation.

  1. abbrev OAI.ThreeState.Spin line 9

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:7 (same declaration text).

  2. def OAI.ThreeState.Admissible line 12

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:10 (same declaration text).

  3. def OAI.ThreeState.channel line 15

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:13 (same declaration text).

  4. def OAI.ThreeState.Observation line 20

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:18 (same declaration text).

  5. theorem OAI.ThreeState.channel_nonneg line 24

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:22 (same declaration text).

  6. theorem OAI.ThreeState.channel_sum line 33

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:31 (same declaration text).

  7. def OAI.ThreeState.channelPMF line 36

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:34 (same declaration text).

  8. def OAI.ThreeState.iidList line 42

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:40 (same declaration text).

  9. def OAI.ThreeState.observedLaw line 48

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:46 (same declaration text).

  10. def OAI.ThreeState.uniformSpin line 55

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:53 (same declaration text).

  11. def OAI.ThreeState.marginal line 60

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:58 (same declaration text).

  12. def OAI.ThreeState.posterior line 64

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:62 (same declaration text).

  13. def OAI.ThreeState.advantage line 70

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:68 (same declaration text).

  14. def OAI.ThreeState.regularLaw line 74

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:72 (same declaration text).

  15. def OAI.ThreeState.poissonOffspring line 78

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:76 (same declaration text).

  16. def OAI.ThreeState.poissonLaw line 85

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:83 (same declaration text).

  17. def OAI.ThreeState.regularAdvantage line 89

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:87 (same declaration text).

  18. def OAI.ThreeState.poissonAdvantage line 92

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:90 (same declaration text).

  19. def OAI.ThreeState.Reconstructs line 97

    Also declared: ComparatorChallenges/ThreeStateSupercritical.lean:95 (same declaration text).

  20. def OAI.ThreeState.Nonreconstructs line 101
  21. def OAI.ThreeState.mass line 107
  22. lemma OAI.ThreeState.mass_nonneg line 109
  23. lemma OAI.ThreeState.mass_sum line 110
  24. lemma OAI.ThreeState.mass_summable line 113
  25. lemma OAI.ThreeState.mass_bind line 116
  26. lemma OAI.ThreeState.mass_uniform line 121
  27. lemma OAI.ThreeState.mass_marginal line 124
  28. lemma OAI.ThreeState.mass_eq_zero line 130
  29. lemma OAI.ThreeState.marginal_zero line 133
  30. lemma OAI.ThreeState.posterior_nonneg line 141
  31. lemma OAI.ThreeState.posterior_sum line 146
  32. lemma OAI.ThreeState.weighted_posterior line 160
  33. lemma OAI.ThreeState.weighted_abs_posterior line 172
  34. lemma OAI.ThreeState.mass_le_one line 181
  35. def OAI.ThreeState.tvMass line 184
  36. lemma OAI.ThreeState.mass_diff_summable line 187
  37. lemma OAI.ThreeState.tvMass_nonneg line 191
  38. lemma OAI.ThreeState.tvMass_le_one line 194
  39. lemma OAI.ThreeState.advantage_eq_tvMass line 203
  40. lemma OAI.ThreeState.advantage_nonneg line 219
  41. lemma OAI.ThreeState.advantage_le_one line 223
  42. lemma OAI.ThreeState.kernel_mass_summable line 229
  43. lemma OAI.ThreeState.weighted_kernel_summable line 235
  44. lemma OAI.ThreeState.mass_diff_bind_le line 241
  45. lemma OAI.ThreeState.tvMass_bind_le line 252
  46. lemma OAI.ThreeState.marginal_bind line 272
  47. theorem OAI.ThreeState.advantage_bind_le line 277