OAI/Probability/ThreeStateClauses/RegularCritical.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Regular Critical.

  1. lemma OAI.ThreeState.TreeClauses.Tree.regular_positive_critical_mu line 17
  2. lemma OAI.ThreeState.TreeClauses.Tree.regular_advantage_sq_bound line 36
  3. theorem OAI.ThreeState.TreeClauses.Tree.regular_positive_critical_nonreconstruction line 47
  4. lemma OAI.ThreeState.TreeClauses.Tree.channelWeight_alt line 74
  5. lemma OAI.ThreeState.TreeClauses.Tree.channelWeight_compose line 79
  6. lemma OAI.ThreeState.TreeClauses.Tree.channel_compose line 91
  7. lemma OAI.ThreeState.TreeClauses.Tree.channel_permute line 104
  8. def OAI.ThreeState.TreeClauses.Tree.relabelRegular line 122
  9. lemma OAI.ThreeState.TreeClauses.Tree.regularLaw_permute line 126
  10. def OAI.ThreeState.TreeClauses.Tree.channelNoise line 143
  11. lemma OAI.ThreeState.TreeClauses.Tree.regularLaw_noise line 150
  12. lemma OAI.ThreeState.TreeClauses.Tree.regular_advantage_sq_moment line 189
  13. lemma OAI.ThreeState.TreeClauses.Tree.regular_channel_mu_le line 199
  14. theorem OAI.ThreeState.TreeClauses.Tree.regular_positive_nonreconstruction line 206