OAI/InformationTheory/Entanglement/BooleanSpan.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteConstruction.monomial line 12
2. def OAI.FiniteConstruction.smallSets line 14
3. lemma OAI.FiniteConstruction.mem_smallSets line 16
4. def OAI.FiniteConstruction.lowDegree line 25
5. lemma OAI.FiniteConstruction.monomial_mem line 28
6. lemma OAI.FiniteConstruction.monomial_empty line 32
7. lemma OAI.FiniteConstruction.monomial_mul line 34
8. lemma OAI.FiniteConstruction.coordinate_mul_mem line 39
9. lemma OAI.FiniteConstruction.sum_power_mem line 54
10. lemma OAI.FiniteConstruction.interpolation_dimension_bound line 65