OAI/NumberTheory/Ostmann/Construction/ConstituentAtomProductBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Whole-atom interval bounds on the actual transfer support

In particular the word atom retains its selected bin, even though its prime constituents range over a much wider interval.

  1. theorem OAI.Ostmann.constituentTransferWeight_atom_product_bounds line 14