OAI/Probability/ThreeStateClauses/RegularReconstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Regular Reconstruction.

  1. def OAI.ThreeState.TreeClauses.Tree.ksConstant line 17
  2. lemma OAI.ThreeState.TreeClauses.Tree.ksConstant_pos line 19
  3. lemma OAI.ThreeState.TreeClauses.Tree.ksConstant_ge_four line 22
  4. lemma OAI.ThreeState.TreeClauses.Tree.ksConstant_identity line 26
  5. lemma OAI.ThreeState.TreeClauses.Tree.regularStatistic_second line 30
  6. lemma OAI.ThreeState.TreeClauses.Tree.regular_estimator_advantage line 70
  7. theorem OAI.ThreeState.TreeClauses.Tree.regular_reconstructs_above_KS line 103

    Distinct definitions of this name: ComparatorChallenges/ThreeStateTreeClauses.lean:92 (same statement text; different proof or body). Qualify references as OAI.ThreeState.TreeClauses.Tree.regular_reconstructs_above_KS@path.