CompositeBadDensityBound.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.CompositeSupply.base_eq_thinSupplyBase line 11
theorem OAI.Problem337.CompositeSupply.badModuli_block_subset line 19
Source documentation
The variable-pool global exception set embeds into the actual fixed-pool exception block. Both roughness and the energy threshold follow from its definition and the proved unit-mixing contraction.
```
theorem badModuli_block_subset (D : ℕ) (hD : 2 ≤ D) :
    (Finset.Ico D (2 * D)).filter BadModulus ⊆ roughModulusBadBlock D := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.roughModulusBadBlock
theorem OAI.Problem337.CompositeSupply.eventually_badModulus_shell_card_le line 36
Source documentation
An unconditional sparse dyadic count for one global predicate. No unproved rough-divisor, collision, or distribution hypothesis remains.
```
theorem eventually_badModulus_shell_card_le :
    ∀ᶠ j : ℕ in atTop,
      (((Finset.Ico (2 ^ j) (2 ^ (j + 1))).filter BadModulus).card : ℝ) ≤
        ((2 : ℝ) ^ j) ^ (15 / 16 : ℝ) := by
…
```
Mentions: OAI.Problem337.CompositeSupply.BadModulus
theorem OAI.Problem337.CompositeSupply.eventually_badMultiples_card_le line 54
Source documentation
The exceptional original integers have arbitrarily small density. This is the unconditional arithmetic input for the cube-free supply assembly.
```
theorem eventually_badMultiples_card_le :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ Y : ℕ in atTop,
      ((badMultiples Y).card : ℝ) ≤ ε * Y := by
…
```
Mentions: OAI.Problem337.CompositeSupply.badMultiples