OAI/InformationTheory/Entanglement/FiberBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteConstruction.Clique line 10
2. def OAI.FiniteConstruction.HasClique line 12
3. def OAI.FiniteConstruction.orRelation line 14
4. def OAI.FiniteConstruction.fiber line 17
5. lemma OAI.FiniteConstruction.mem_fiber line 20
6. lemma OAI.FiniteConstruction.card_fibers line 22
7. lemma OAI.FiniteConstruction.join_cliques line 30
8. lemma OAI.FiniteConstruction.no_pair_of_no_clique_two line 74
9. lemma OAI.FiniteConstruction.amplification_bound line 90