OAI/NumberTheory/JointDickman/Amplification/NumericAdditionWeights.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.prime_product_weight_le_residue_product line 11
2. theorem OAI.JointDickman.prefix_count_weight_le_residue_product line 29
3. theorem OAI.JointDickman.regular_numeric_addition_majorant line 46

   Source documentation

   Prefix regularity of the alternative quotient supplies its half-weight. Deleting all other prime conditions increases the numeric sum.

   theorem regular_numeric_addition_majorant {B L k n : ℕ} {τ C q : ℝ}
       (S P : Finset ℕ) (hn : n ≠ 0) (hk : k ∈ Icc 1 L)
       (hreg : RegularPrimeSet B L τ C (coefficientPrimeSet B n))
       (hP : P ⊆ primePrefix B ((k : ℝ)/L) (auxiliaryPrimes B))
       (hS : ∀ p ∈ S, p.Prime) (hq : 0 ≤ q) (hq1 : q ≤ 1) :
       q^S.card ≤ Real.exp (((((k : ℝ)/L)/2+τ)*auxiliaryLogLength B)*Real.log 2)*
         ∏ p ∈ P, residueWeight q 0 ((∏ r ∈ S, r : ℕ) : ZMod p)*residueWeight (1/2) 0 (n : ZMod p) := by
   …

   Mentions: OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.primePrefix, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryLogLength, OAI.JointDickman.residueWeight