OAI/NumberTheory/OrdinaryCorrelations/HighTrace/RankBot.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceCylinder.rank_bot line 23
2. lemma OAI.OrdinaryCorrelations.SourceCylinder.witness_dominating line 38
3. lemma OAI.OrdinaryCorrelations.SourceCylinder.ideal_card_bound line 96
4. lemma OAI.OrdinaryCorrelations.SourceCylinder.witnesses_width line 109
5. lemma OAI.OrdinaryCorrelations.SourceCylinder.retained_coefficient_bound line 115
6. lemma OAI.OrdinaryCorrelations.SourceCylinder.satisfied_retained_card_bound line 124
7. lemma OAI.OrdinaryCorrelations.SourceCylinder.truncation_exact_of_low_rank line 149
8. lemma OAI.OrdinaryCorrelations.SourceCylinder.truncation_bound line 164