RoughModulusBlocks.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.roughModulusBadBlock line 13
Source documentation
Bad moduli on one block use one common divisor list. This deliberate fixed-base choice is needed for the off-diagonal double count.
```
def roughModulusBadBlock (D : ℕ) : Finset ℕ := by
…
```
Mentions: OAI.Problem337.D
theorem OAI.Problem337.roughModulusBadBlock_card_le line 21
lemma OAI.Problem337.roughModulusBlock_power_budget line 59
Source documentation
The small subpower divisor error still leaves a fixed power saving in the bad-modulus count, including the dyadic-block factor of two.
```
lemma roughModulusBlock_power_budget {D : ℝ} (hD : 0 < D)
    (hlarge : 4 ≤ D ^ (1 / 32 : ℝ)) :
    2 * (2 * D) ^ (7 / 8 : ℝ) * (2 * D) ^ (1 / 32 : ℝ) ≤
      D ^ (15 / 16 : ℝ) := by
…
```
Mentions: OAI.Problem337.D

theorem OAI.Problem337.eventually_roughModulusBadBlock_card_le_of_divisor_subpower line 86

Source documentation

The actual prime-prefix cardinality and size estimates discharge all inputs to the block double count except the uniform restricted-divisor estimate. That estimate concerns arbitrary positive differences, not rough ambient integers.

theorem eventually_roughModulusBadBlock_card_le_of_divisor_subpower
    (hrough : ∀ᶠ X : ℝ in atTop, ∀ n : ℕ, n ≠ 0 →
      Real.log (n : ℝ) ≤ (2 / Real.log 2 + 1) * Real.log X * Real.log (Real.log X) →
      ((n.divisors.filter (fun d : ℕ => (d : ℝ) ≤ X ∧
        ∀ p ∈ d.primeFactorsList, Real.log X ≤ (p : ℝ))).card : ℝ) ≤
        X ^ (1 / 32 : ℝ)) :
    ∀ᶠ D : ℕ in atTop,
      ((roughModulusBadBlock D).card : ℝ) ≤ (D : ℝ) ^ (15 / 16 : ℝ) := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.roughModulusBadBlock

theorem OAI.Problem337.eventually_roughModulusBadBlock_card_le line 129
Source documentation
An unconditional power-saving bound for the actual bad-modulus blocks. The common divisor list is the explicit logarithmic prime prefix, and the restricted-divisor estimate has been discharged for every positive difference.
```
theorem eventually_roughModulusBadBlock_card_le :
    ∀ᶠ D : ℕ in atTop,
      ((roughModulusBadBlock D).card : ℝ) ≤ (D : ℝ) ^ (15 / 16 : ℝ) := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.roughModulusBadBlock