OAI/Analysis/JiangSu/DimensionDrop/TwoScaleMatching.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JiangSuConstruction.continuous_matching_control_two_scales line 14
2. lemma OAI.JiangSuConstruction.filter_card_equiv line 58
3. abbrev OAI.JiangSuConstruction.iteratedSize line 66
4. def OAI.JiangSuConstruction.iteratedTuple line 67
5. lemma OAI.JiangSuConstruction.iteratedTuple_continuous line 70
6. lemma OAI.JiangSuConstruction.iteratedTuple_shifted_counts line 75
7. lemma OAI.JiangSuConstruction.finite_continuous_modulus line 93
8. theorem OAI.JiangSuConstruction.actual_iterated_continuous_matching line 109