LocalProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the finite product of local moment bounds

The local factors in Section 3 of paper 031-01 are uniformly bounded. For every positive exponent, their product over distinct prime divisors of the saturation index is therefore bounded by a constant times that index to the given exponent. This elementary argument also works for any finite set of distinct positive integers.

theorem OAI.DukePrimeDegree.prod_le_subpower_of_uniform_bound line 24

Source documentation

A finite product of uniformly bounded factors has arbitrarily small power growth in the product of its distinct positive integer labels.

theorem prod_le_subpower_of_uniform_bound
    (f : ℕ → ℝ) (B ε : ℝ) (hB : 1 ≤ B) (hε : 0 < ε)
    (hf : ∀ p, 0 ≤ f p ∧ f p ≤ B) :
    ∃ C : ℝ, 0 < C ∧ ∀ s : Finset ℕ, (∀ p ∈ s, 1 ≤ p) →
      (∏ p ∈ s, f p) ≤ C * (∏ p ∈ s, (p : ℝ)) ^ ε := by
…

theorem OAI.DukePrimeDegree.prod_le_index_subpower line 60

Source documentation

The specialization used when all local labels divide the index, so their product is at most that index.

theorem prod_le_index_subpower
    (f : ℕ → ℝ) (B ε : ℝ) (hB : 1 ≤ B) (hε : 0 < ε)
    (hf : ∀ p, 0 ≤ f p ∧ f p ≤ B) :
    ∃ C : ℝ, 0 < C ∧ ∀ (s : Finset ℕ) (q : ℝ),
      (∀ p ∈ s, 1 ≤ p) → (∏ p ∈ s, (p : ℝ)) ≤ q →
      (∏ p ∈ s, f p) ≤ C * q ^ ε := by
…