OAI/NumberTheory/OrdinaryCorrelations/HighTrace/IntersectionEqBotOfSupport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceCylinder.intersection_eq_bot_of_support_empty line 23
2. lemma OAI.OrdinaryCorrelations.SourceCylinder.coefficient_support_one line 27
3. lemma OAI.OrdinaryCorrelations.SourceCylinder.coefficient_support_bound line 46
4. lemma OAI.OrdinaryCorrelations.SourceCylinder.max_power_mono line 58
5. def OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.on line 70
6. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.on_support line 73
7. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.on_holds line 79
8. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.le_on line 85
9. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.on_le line 91
10. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.generates_on line 103
11. def OAI.OrdinaryCorrelations.SourceCylinder.active line 115
12. def OAI.OrdinaryCorrelations.SourceCylinder.atPoint line 119
13. lemma OAI.OrdinaryCorrelations.SourceCylinder.atPoint_holds line 125
14. lemma OAI.OrdinaryCorrelations.SourceCylinder.holds_iff_le_atPoint line 129
15. lemma OAI.OrdinaryCorrelations.SourceCylinder.atPoint_bot_iff line 142
16. lemma OAI.OrdinaryCorrelations.SourceCylinder.full_sum_holds line 165