OAI/Probability/ThreeState/Negative.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Signed small-channel and Dobrushin non-reconstruction regions.

  1. theorem OAI.ThreeState.regular_small_negative_nonreconstruction line 15
  2. theorem OAI.ThreeState.poisson_small_negative_nonreconstruction line 47
  3. lemma OAI.ThreeState.compose_pairTV_bound line 87
  4. lemma OAI.ThreeState.ordered_pairTV_decay line 130
  5. theorem OAI.ThreeState.nonreconstruction_dobrushin line 156
  6. theorem OAI.ThreeState.regular_dobrushin_nonreconstruction line 180
  7. theorem OAI.ThreeState.poisson_dobrushin_nonreconstruction line 192
  8. theorem OAI.ThreeState.binary_negative_nonreconstruction line 204
  9. theorem OAI.ThreeState.poisson_le_two_negative_nonreconstruction line 213