OAI/NumberTheory/Ostmann/Supply/WeightPointwiseBound.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Supply.card_retained_subsets_leline 10 - theorem
OAI.Ostmann.Supply.truncatedWeight_le_card_boundline 31 - theorem
OAI.Ostmann.Supply.sparseKernel_pointwise_le_oneline 57 - theorem
OAI.Ostmann.Supply.truncatedKernelWeight_pointwise_leline 72