OAI/NumberTheory/JointDickman/Amplification/AmplificationVolumeProducts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.baseArithmeticResidueWeight line 12
2. def OAI.JointDickman.baseArithmeticResidueMean line 15
3. theorem OAI.JointDickman.baseArithmeticResidueWeight_product line 18
4. theorem OAI.JointDickman.baseArithmeticResidueWeight_mean line 24
5. theorem OAI.JointDickman.coefficient_harmonic_product line 41
6. theorem OAI.JointDickman.coefficient_harmonic_mul_residueMean_le line 54

   Source documentation

   This exact finite cancellation bounds the Cauchy volume without a further interval asymptotic: the leftover Euler factors are at most one.

   theorem coefficient_harmonic_mul_residueMean_le {B : ℕ} (hB : 1 < B) :
       (∑ D ∈ (auxiliaryPrimes B).powerset,
         coefficientWeight B (∏ p ∈ D, p) / (∏ p ∈ D, (p : ℝ))) *
         baseArithmeticResidueMean B ≤ B := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.coefficientWeight, OAI.JointDickman.baseArithmeticResidueMean