OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Witness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.SourceCylinder.Witness line 17
2. lemma OAI.OrdinaryCorrelations.SourceCylinder.exists_witnessGenerator line 21
3. def OAI.OrdinaryCorrelations.SourceCylinder.witnessGenerator line 47
4. lemma OAI.OrdinaryCorrelations.SourceCylinder.witnessGenerator_spec line 51
5. lemma OAI.OrdinaryCorrelations.SourceCylinder.witnessGenerator_injective line 58
6. lemma OAI.OrdinaryCorrelations.SourceCylinder.witnessGenerator_holds line 67
7. lemma OAI.OrdinaryCorrelations.SourceCylinder.witnessCount_eq_sum line 77
8. theorem OAI.OrdinaryCorrelations.SourceCylinder.witnessCount_le_list_sum line 85