OAI/NumberTheory/JointDickman/Amplification/BinCofactorBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.bin_prime_above_first_root line 11
2. lemma OAI.JointDickman.binLabel_small_prime_power line 22
3. lemma OAI.JointDickman.binLabel_fixed_product_invariant line 33
4. theorem OAI.JointDickman.bin_cofactor_away_zero line 52

   Source documentation

   The functions here are exactly the manuscript's bin labels with a fixed finite-prime weight. Only the explicit prime-scale inequalities remain.

   theorem bin_cofactor_away_zero {J : ℕ} (hJ : 0 < J) {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
       (E : Finset ℕ) (hE : ∀ p ∈ E, p.Prime) {ε : ℝ} (hε : 0 < ε) :
       ∃ T : ℝ, ∃ K : ℕ, 0 < T ∧ 2 ≤ K ∧
       ∀ (N : ℕ) (a x : ℝ), 1 ≤ a → 1 ≤ x → K ≤ ⌊(N:ℝ)/a⌋₊ →
         (⌊(2*N:ℝ)/a⌋₊:ℝ)^c ≤ x^((1:ℝ)/J) →
         (∀ p ∈ E, (p:ℝ) ≤ x^((1:ℝ)/J)) →
         ∀ (ζ : Fin (J-1) → ℂ), (∀ i, ‖ζ i‖ ≤ 1) →
         ∀ P : Finset ℕ, (∀ p ∈ P, p.Prime ∧
           (⌊(2*N:ℝ)/a⌋₊:ℝ)^c < (p:ℝ) ∧ (p:ℝ) ≤ (⌊(N:ℝ)/a⌋₊:ℝ)) →
         Disjoint E P → ∀ w : ℕ → ℝ, (∀ p ∈ E, 0 ≤ w p ∧ w p ≤ 1) →
         ∀ t : ℝ, T ≤ |t| → |t| ≤ (⌊(2*N:ℝ)/a⌋₊:ℝ)^2 →
         ‖mrtCofactorPolynomial P
   …