Maximal-divisor bounds

This file proves the finite-poset cover behind the paper's maximal-divisor improvement and combines it with the new joint p - 1, p + 1 estimate.

def BGS.NumberTheory.maximalDivisorsBelow (n bound : ℕ) : Finset ℕ

Divisors of n maximal under divisibility among those strictly below bound.

Equations

• BGS.NumberTheory.maximalDivisorsBelow n bound = {d ∈ n.divisors | d < bound ∧ ∀ e ∈ n.divisors, e < bound → d ∣ e → e = d}

@[simp]

theorem BGS.NumberTheory.mem_maximalDivisorsBelow_iff {n bound d : ℕ} : d ∈ maximalDivisorsBelow n bound ↔ d ∈ n.divisors ∧ d < bound ∧ ∀ e ∈ n.divisors, e < bound → d ∣ e → e = d

theorem BGS.NumberTheory.maximalDivisorsBelow_subset_divisors (n bound : ℕ) : maximalDivisorsBelow n bound ⊆ n.divisors

theorem BGS.NumberTheory.maximalDivisorsBelow_card_le_card_divisors (n bound : ℕ) : (maximalDivisorsBelow n bound).card ≤ n.divisors.card

theorem BGS.NumberTheory.exists_dvd_maximalDivisorBelow {n bound d : ℕ} (hn : n ≠ 0) (hdn : d ∣ n) (hdbound : d < bound) : ∃ m ∈ maximalDivisorsBelow n bound, d ∣ m

Every divisor below the cutoff divides a maximal divisor below it.

def BGS.NumberTheory.elementsWithPowOne (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (m : ℕ) : Finset G

Elements killed by the m-th power map.

Equations

• BGS.NumberTheory.elementsWithPowOne G m = {g : G | g ^ m = 1}

@[simp]

theorem BGS.NumberTheory.mem_elementsWithPowOne_iff (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] {m : ℕ} {g : G} : g ∈ elementsWithPowOne G m ↔ g ^ m = 1

theorem BGS.NumberTheory.elementsOfOrderLessThan_subset_maximalDivisorCover (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (bound : ℕ) : {g : G | orderOf g < bound} ⊆ (maximalDivisorsBelow (Fintype.card G) bound).biUnion (elementsWithPowOne G)

Low-order elements in a cyclic group are covered by roots-of-unity sets indexed by maximal divisors.

theorem BGS.NumberTheory.elementsOfOrderLessThan_card_le_maximalDivisors (G : Type u_1) [Group G] [Fintype G] [IsCyclic G] (bound : ℕ) : {g : G | orderOf g < bound}.card ≤ (bound - 1) * (maximalDivisorsBelow (Fintype.card G) bound).card

The cyclic low-order count using only maximal divisors.

theorem BGS.NumberTheory.maximalDivisorCounts_product_pow_ten_le {p bound : ℕ} (hp : Odd p) (hpTwo : 2 < p) : ((maximalDivisorsBelow (p - 1) bound).card * (maximalDivisorsBelow (p + 1) bound).card) ^ 10 ≤ 2 ^ 457 * (p ^ 2 - 1)

The two maximal-divisor counts inherit the exact joint tenth moment.

theorem BGS.NumberTheory.maximalDivisorCounts_add_sq_le {p bound C J : ℕ} (hminus : (maximalDivisorsBelow (p - 1) bound).card ≤ C) (hplus : (maximalDivisorsBelow (p + 1) bound).card ≤ C) (hproduct : (maximalDivisorsBelow (p - 1) bound).card * (maximalDivisorsBelow (p + 1) bound).card ≤ J) : ((maximalDivisorsBelow (p - 1) bound).card + (maximalDivisorsBelow (p + 1) bound).card) ^ 2 ≤ C ^ 2 + 3 * J

The new square envelope for the sum of the two maximal-divisor counts.