BinCounts.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Bounded multiplicity counts and smoothness at bin endpoints

A product of the prime powers counted in a bin divides the integer. This bounds every bin count uniformly on fixed windows n ≤ C*x. The endpoint criterion identifies smoothness with vanishing counts in all higher bins.

theorem OAI.JointDickman.mem_primeBin_iff line 19
theorem OAI.JointDickman.bin_primePower_prod_dvd line 33
Source documentation
The product of the complete prime powers selected by a finite bin divides n.
```
theorem bin_primePower_prod_dvd (E : Finset ℕ) (n : ℕ) :
    (∏ p ∈ E, p ^ n.factorization p) ∣ n := by
…
```

theorem OAI.JointDickman.binCount_pow_le line 53

Source documentation

A lower bound for every counted prime gives a power lower bound for n.

theorem binCount_pow_le (E : Finset ℕ) {n : ℕ} (hn : n ≠ 0)
    {q : ℝ} (hq : 0 ≤ q) (hE : ∀ p ∈ E, q ≤ (p : ℝ)) :
    q ^ binCount E n ≤ (n : ℝ) := by
…

Mentions: OAI.JointDickman.binCount

theorem OAI.JointDickman.primeBin_count_eventually_le line 67
Source documentation
Uniform boundedness of every relevant count, sufficient for interpolation. The bound holds simultaneously for all bin indices k ≥ 1.
```
theorem primeBin_count_eventually_le (J : ℕ) (hJ : 0 < J) (C : ℝ) :
    ∀ᶠ x : ℝ in atTop, ∀ k : ℕ, 1 ≤ k → ∀ n : ℕ, 1 ≤ n →
      (n : ℝ) ≤ C * x → binCount (primeBin x J k) n ≤ J := by
…
```
Mentions: OAI.JointDickman.binCount, OAI.JointDickman.primeBin

theorem OAI.JointDickman.exists_adjacent_crossing line 97

Source documentation

A finite sequence crossing a level has an adjacent pair straddling it.

private theorem exists_adjacent_crossing (y : ℕ → ℝ) (a : ℝ) {d : ℕ}
    (hzero : y 0 < a) (hend : a ≤ y d) :
    ∃ k : ℕ, k < d ∧ y k < a ∧ a ≤ y (k + 1) := by
…

theorem OAI.JointDickman.exists_higher_primeBin line 109

Source documentation

Every number between a bin endpoint and x belongs to a higher bin.

theorem exists_higher_primeBin {x : ℝ} (hx : 0 ≤ x) {J r p : ℕ}
    (hJ : 0 < J) (hr : r ≤ J) (hp : p.Prime)
    (hlow : x ^ ((r : ℝ) / J) < (p : ℝ)) (hhigh : (p : ℝ) ≤ x) :
    ∃ k ∈ Finset.Ico r J, p ∈ primeBin x J k := by
…

Mentions: OAI.JointDickman.primeBin

theorem OAI.JointDickman.maxPrimeFac_le_iff_higher_counts_zero line 129

Source documentation

Smoothness at a rational endpoint is exactly vanishing of the higher-bin multiplicity counts, provided 1 ≤ n ≤ x.

theorem maxPrimeFac_le_iff_higher_counts_zero {x : ℝ} (hx : 1 ≤ x)
    {J r n : ℕ} (hJ : 0 < J) (hr : r ≤ J) (hn : 1 ≤ n) (hnx : (n : ℝ) ≤ x) :
    (n.maxPrimeFac : ℝ) ≤ x ^ ((r : ℝ) / J) ↔
      ∀ k ∈ Finset.Ico r J, binCount (primeBin x J k) n = 0 := by
…

Mentions: OAI.JointDickman.binCount, OAI.JointDickman.primeBin

theorem OAI.JointDickman.centered_binLabel_interpolation_on_window line 167

Source documentation

The fixed coefficient vector from interpolation works on every fixed window n ≤ C*x, once the scale is sufficiently large.

theorem centered_binLabel_interpolation_on_window {ι : Type*} [Fintype ι] [DecidableEq ι]
    (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
    (ζ : ι → ℂ) (μ : ℂ) (C : ℝ) :
    ∃ c : (ι → Fin (J + 1)) → ℂ, ∀ᶠ x : ℝ in atTop,
      ∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ C * x →
        binLabel (fun i => primeBin x J (k i)) ζ n - μ =
          ∑ a : ι → Fin (J + 1), c a *
            (binLabel (fun i => primeBin x J (k i))
              (fun i => interpolationNode (a i)) n : ℂ) := by
…

Mentions: OAI.JointDickman.binLabel, OAI.JointDickman.primeBin, OAI.JointDickman.interpolationNode