OAI/NumberTheory/Ostmann/Construction/InitialHalfBulkProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lower product bounds for the two genuine half-bulk cutoffs

  1. theorem OAI.Ostmann.initialHalfBulkWeight_product_lower line 9
  2. theorem OAI.Ostmann.initialHalfBulkProduct_product_lower line 25