OAI/Computability/QuantumFactoring/CoveringPowerEmission.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NetworkEmission.bits_length_max_le line 14
2. lemma OAI.ExactQuantumFactoring.NetworkEmission.tokenCode_length_append line 18
3. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprCode_ite_le line 21
4. def OAI.ExactQuantumFactoring.NetworkEmission.coveringStep line 35
5. lemma OAI.ExactQuantumFactoring.NetworkEmission.coveringStep_pow line 37
6. lemma OAI.ExactQuantumFactoring.NetworkEmission.coveringStep_base line 43
7. lemma OAI.ExactQuantumFactoring.NetworkEmission.coveringStep_pow_size line 48
8. lemma OAI.ExactQuantumFactoring.NetworkEmission.coveringStep_expr_bound line 55
9. lemma OAI.ExactQuantumFactoring.NetworkEmission.coveringStep_start line 72
10. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.coveringPowP line 78
11. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.coveringPow line 109