OAI/NumberTheory/TwoPoint/Bounds/PrimeDefectCRT.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The ordinary mean of the finite prime-defect majorant is computed by CRT modulo the squared primes. Only the finite interval boundary remains.

  1. lemma OAI.TwoPointCorrelations.uniformAverage_pi_product line 14

    Distinct definitions of this name: OAI/NumberTheory/TwoPoint/Bounds/ActualPaddingIntegerBounds.lean:15 (different declaration text). Qualify references as OAI.TwoPointCorrelations.uniformAverage_pi_product@path.

  2. lemma OAI.TwoPointCorrelations.primeDefectMajorant_crt_bound line 21