OAI/Probability/SwitchChain/Main.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.switch_chain_main line 18

   Distinct definitions of this name: ComparatorChallenges/SwitchChain.lean:155 (same statement text; different proof or body). Qualify references as OAI.Problem315.switch_chain_main@path.

2. theorem OAI.Problem315.switch_chain_tv_bound line 30

   Distinct definitions of this name: ComparatorChallenges/SwitchChain.lean:159 (same statement text; different proof or body). Qualify references as OAI.Problem315.switch_chain_tv_bound@path.

3. theorem OAI.Problem315.switch_connectivity line 36

   Distinct definitions of this name: ComparatorChallenges/SwitchChain.lean:163 (same statement text; different proof or body). Qualify references as OAI.Problem315.switch_connectivity@path.