CompositeBadDensity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.CompositeSupply.badMultiples line 14
Source documentation
Integers containing a global bad conductor above the logarithmic cutoff. This finite set depends only on the ambient range, not on any chosen modulus.
```
def badMultiples (Y : ℕ) : Finset ℕ := by
…
```
lemma OAI.Problem337.CompositeSupply.mem_badMultiples_iff line 19
lemma OAI.Problem337.CompositeSupply.not_bad_of_not_mem_badMultiples line 28
Source documentation
Every conductor of a residual modulus avoids the global bad set if its original positive multiple avoids badMultiples.
```
lemma not_bad_of_not_mem_badMultiples {Y n q d : ℕ}
    (hn : 1 ≤ n) (hnY : n ≤ Y) (hqn : q ∣ n)
    (hc : (base Y).Coprime q) (hne : n ∉ badMultiples Y)
    (hdq : d ∣ q) (hd : 2 ≤ d) : ¬ BadModulus d := by
…
```
Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.badMultiples, OAI.Problem337.CompositeSupply.BadModulus

lemma OAI.Problem337.CompositeSupply.ambient_collisions_le_of_not_mem_badMultiples line 42

Source documentation

Quantitative conductor collisions for the global divisor pool, uniformly for every residual divisor of an integer outside the one exceptional set.

lemma ambient_collisions_le_of_not_mem_badMultiples {Y n q d : ℕ} [NeZero d]
    (hn : 1 ≤ n) (hnY : n ≤ Y) (hqn : q ∣ n)
    (hc : (base Y).Coprime q) (hne : n ∉ badMultiples Y)
    (hdq : d ∣ q) (hd : 2 ≤ d) :
    ((collisionPairs (base Y).divisors (fun a => a % d)).card : ℝ) ≤
      ((base Y).divisors.card : ℝ)^2 / (d : ℝ)^(7 / 8 : ℝ) := by
…

Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.badMultiples, OAI.Problem337.collisionPairs

theorem OAI.Problem337.CompositeSupply.eventually_badMultiples_card_le_of_shell_bound line 56
Source documentation
A sublinear shell count gives a vanishing exceptional-multiple density at the actual logarithmic conductor cutoff. The shell hypothesis is the only input; the cutoff and the product-energy transport are unconditional.
```
theorem eventually_badMultiples_card_le_of_shell_bound
    {C β : ℝ} (hC : 0 ≤ C) (hβ : β < 1)
    (hcount : ∀ᶠ j : ℕ in atTop,
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter BadModulus).card : ℝ) ≤
        C * ((2 : ℝ) ^ j) ^ β) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ Y : ℕ in atTop,
      ((badMultiples Y).card : ℝ) ≤ ε * Y := by
…
```
Mentions: OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.CompositeSupply.badMultiples