SparseBadDivisorTail.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.SparseBadDivisorTail.sum_dyadic_from line 10

Source documentation

Dyadic decomposition starting at an arbitrary dyadic threshold.

lemma sum_dyadic_from {M : Type*} [AddCommMonoid M]
    (f : ℕ → M) (J K : ℕ) :
    (∑ n ∈ Finset.Ico (2 ^ J) (2 ^ (J + K)), f n) =
      ∑ k ∈ Finset.range K,
        ∑ n ∈ Finset.Ico (2 ^ (J + k)) (2 ^ (J + k + 1)), f n := by
…

lemma OAI.Problem337.SparseBadDivisorTail.reciprocal_shell_le line 24

Source documentation

A dyadic shell has reciprocal mass at most its cardinality over its base.

lemma reciprocal_shell_le (A : Finset ℕ) (j : ℕ) :
    (∑ n ∈ Finset.Ico (2 ^ j) (2 ^ (j + 1)) ∩ A, (1 : ℝ) / n) ≤
      ((Finset.Ico (2 ^ j) (2 ^ (j + 1)) ∩ A).card : ℝ) / (2 : ℝ) ^ j := by
…

theorem OAI.Problem337.SparseBadDivisorTail.reciprocal_tail_le line 40

Source documentation

Finite reciprocal-tail estimate from dyadic cardinality bounds. The geometric ratio r is the shell-growth ratio divided by two. Only shells at or above J need satisfy the estimate.

theorem reciprocal_tail_le (A : Finset ℕ) (J : ℕ) {C r : ℝ}
    (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1)
    (hA : ∀ n ∈ A, 2 ^ J ≤ n)
    (hcount : ∀ j : ℕ, J ≤ j →
      ((Finset.Ico (2 ^ j) (2 ^ (j + 1)) ∩ A).card : ℝ) ≤ C * (2 * r) ^ j) :
    (∑ n ∈ A, (1 : ℝ) / n) ≤ C * r ^ J / (1 - r) := by
…

def OAI.Problem337.SparseBadDivisorTail.divisorMultiples line 92
Source documentation
Positive integers up to Y divisible by at least one member of A.
```
def divisorMultiples (A : Finset ℕ) (Y : ℕ) : Finset ℕ :=
…
```
lemma OAI.Problem337.SparseBadDivisorTail.card_positive_multiples line 95
theorem OAI.Problem337.SparseBadDivisorTail.divisorMultiples_card_le line 105
Source documentation
The union bound for exceptional divisors has no additive endpoint error.
```
theorem divisorMultiples_card_le (A : Finset ℕ) (Y : ℕ) :
    ((divisorMultiples A Y).card : ℝ) ≤
      (Y : ℝ) * ∑ d ∈ A, (1 : ℝ) / d := by
…
```
Mentions: OAI.Problem337.SparseBadDivisorTail.divisorMultiples
def OAI.Problem337.SparseBadDivisorTail.badTail line 127
Source documentation
A finite piece of a global exceptional-modulus predicate above 2^J.
```
def badTail (B : ℕ → Prop) [DecidablePred B] (J Y : ℕ) : Finset ℕ :=
…
```

theorem OAI.Problem337.SparseBadDivisorTail.badTail_reciprocal_le line 131

Source documentation

Global dyadic counts control every finite truncation of the reciprocal tail.

theorem badTail_reciprocal_le (B : ℕ → Prop) [DecidablePred B]
    (J Y : ℕ) {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1)
    (hcount : ∀ j : ℕ, J ≤ j →
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter B).card : ℝ) ≤ C * (2 * r) ^ j) :
    (∑ d ∈ badTail B J Y, (1 : ℝ) / d) ≤ C * r ^ J / (1 - r) := by
…

Mentions: OAI.Problem337.SparseBadDivisorTail.badTail

theorem OAI.Problem337.SparseBadDivisorTail.badTail_multiples_card_le line 151

Source documentation

Uniform exceptional-multiple density, with the explicit geometric tail.

theorem badTail_multiples_card_le (B : ℕ → Prop) [DecidablePred B]
    (J Y : ℕ) {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1)
    (hcount : ∀ j : ℕ, J ≤ j →
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter B).card : ℝ) ≤ C * (2 * r) ^ j) :
    ((divisorMultiples (badTail B J Y) Y).card : ℝ) ≤
      (Y : ℝ) * (C * r ^ J / (1 - r)) := by
…

Mentions: OAI.Problem337.SparseBadDivisorTail.divisorMultiples, OAI.Problem337.SparseBadDivisorTail.badTail

theorem OAI.Problem337.SparseBadDivisorTail.eventually_badTail_multiples_small line 164

Source documentation

Dyadic sublinear exceptional counts give a density tending uniformly to zero as the excluded divisor threshold grows. The onset of the shell estimate may be arbitrary but fixed.

theorem eventually_badTail_multiples_small (B : ℕ → Prop) [DecidablePred B]
    (J₀ : ℕ) {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1)
    (hcount : ∀ j : ℕ, J₀ ≤ j →
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter B).card : ℝ) ≤ C * (2 * r) ^ j) :
    ∀ ε : ℝ, 0 < ε → ∃ J₁ : ℕ, J₀ ≤ J₁ ∧ ∀ J : ℕ, J₁ ≤ J → ∀ Y : ℕ,
      ((divisorMultiples (badTail B J Y) Y).card : ℝ) ≤ ε * Y := by
…

Mentions: OAI.Problem337.SparseBadDivisorTail.divisorMultiples, OAI.Problem337.SparseBadDivisorTail.badTail

theorem OAI.Problem337.SparseBadDivisorTail.eventually_badTail_multiples_small_of_power line 191

Source documentation

The usual sublinear-power form of the uniform density statement.

theorem eventually_badTail_multiples_small_of_power (B : ℕ → Prop) [DecidablePred B]
    (J₀ : ℕ) {C β : ℝ} (hC : 0 ≤ C) (hβ : β < 1)
    (hcount : ∀ j : ℕ, J₀ ≤ j →
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter B).card : ℝ) ≤
        C * ((2 : ℝ) ^ j) ^ β) :
    ∀ ε : ℝ, 0 < ε → ∃ J₁ : ℕ, J₀ ≤ J₁ ∧ ∀ J : ℕ, J₁ ≤ J → ∀ Y : ℕ,
      ((divisorMultiples (badTail B J Y) Y).card : ℝ) ≤ ε * Y := by
…

Mentions: OAI.Problem337.SparseBadDivisorTail.divisorMultiples, OAI.Problem337.SparseBadDivisorTail.badTail

lemma OAI.Problem337.SparseBadDivisorTail.divisorMultiples_mono line 214

lemma OAI.Problem337.SparseBadDivisorTail.mem_divisorMultiples_badAbove line 221

Source documentation

The finite divisor cutoff is semantically redundant for positive multiples.

lemma mem_divisorMultiples_badAbove (B : ℕ → Prop) [DecidablePred B]
    (R Y n : ℕ) :
    n ∈ divisorMultiples ((Finset.Icc R Y).filter B) Y ↔
      1 ≤ n ∧ n ≤ Y ∧ ∃ d : ℕ, R ≤ d ∧ B d ∧ d ∣ n := by
…

Mentions: OAI.Problem337.SparseBadDivisorTail.divisorMultiples

theorem OAI.Problem337.SparseBadDivisorTail.eventually_large_bad_divisor_multiples_small line 235

Source documentation

An arbitrary growing lower cutoff can be used, not just a dyadic one. The conclusion is uniform in the ambient integer interval.

theorem eventually_large_bad_divisor_multiples_small (B : ℕ → Prop) [DecidablePred B]
    (J₀ : ℕ) {C β : ℝ} (hC : 0 ≤ C) (hβ : β < 1)
    (hcount : ∀ j : ℕ, J₀ ≤ j →
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter B).card : ℝ) ≤
        C * ((2 : ℝ) ^ j) ^ β) :
    ∀ ε : ℝ, 0 < ε → ∃ R₀ : ℕ, 1 ≤ R₀ ∧ ∀ R : ℕ, R₀ ≤ R → ∀ Y : ℕ,
      ((divisorMultiples ((Finset.Icc R Y).filter B) Y).card : ℝ) ≤ ε * Y := by
…

Mentions: OAI.Problem337.SparseBadDivisorTail.divisorMultiples