OAI/Combinatorics/SumProduct/Alignment/HierarchyRates01.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourceHierarchyRates.source_modulus_size line 28
2. lemma OAI.SourceHierarchyRates.earlier_dominates_modulus line 41
3. lemma OAI.SourceHierarchyRates.eventually_height_ge_modulus_sq line 53
4. lemma OAI.SourceHierarchyRates.eventually_interval_four_modulus line 69
5. lemma OAI.SourceHierarchyRates.raw_interval_tendsto line 86
6. lemma OAI.SourceHierarchyRates.raw_over_modulus_tendsto line 101
7. theorem OAI.SourceHierarchyRates.source_translation_error line 119
8. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_uniform_extension line 195