OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/CapUpper.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OrdinarySmoothRough.capUpperline 22 - lemma
OAI.OrdinarySmoothRough.quarter_floor_comparisonline 24 - lemma
OAI.OrdinarySmoothRough.capUpper_errorline 30 - lemma
OAI.OrdinarySmoothRough.floor_boundary_widthline 37 - lemma
OAI.OrdinarySmoothRough.capped_rough_scaleline 60 - theorem
OAI.OrdinarySmoothRough.capped_slice_defect_sieveline 72