OAI/NumberTheory/OrdinaryCorrelations/HighTrace/WitnessEntropyBase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.witnessEntropyBase line 18
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.witnessEntropyDegree line 21
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.add_one_le_pow_succ line 24
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.witness_polynomial_bound line 30