OAI/NumberTheory/Ostmann/Quadratic/QuadraticDivisorDyadicPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Disjoint divisor blocks, including the divisor-one boundary

  1. def OAI.Ostmann.quadraticDivisorDyadicBlock line 11
  2. theorem OAI.Ostmann.quadraticDivisorDyadicBlock_subset line 14
  3. theorem OAI.Ostmann.quadratic_divisor_dyadic_sum line 27
  4. theorem OAI.Ostmann.quadratic_divisor_sum_one_blocks line 40
  5. theorem OAI.Ostmann.quadratic_divisor_sum_blocks_bound line 52