MinorArcRealWindow.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MinorArc.majorArcUnion_mono_radius line 9
Source documentation
Enlarging the radius enlarges the explicit finite major-arc union.
```
theorem majorArcUnion_mono_radius (Q : ℕ) {δ ε : ℝ} (hδε : δ ≤ ε) :
    ThreePrimeAnalysis.majorArcUnion Q δ ⊆ ThreePrimeAnalysis.majorArcUnion Q ε := by
…
```
Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

theorem OAI.Problem337.MinorArc.exists_minor_fraction_real_window line 21

Source documentation

Dirichlet approximation in the real parameter window used by minor-arc estimates. The scale is rounded only internally; the theorem exposes the usable real inequalities R ≤ q ≤ X/R without floor losses.

theorem exists_minor_fraction_real_window {X R x : ℝ}
    (hR : 0 < R) (hXR : 4 * R ≤ X)
    (hx : x ∈ Set.Icc (0 : ℝ) 1)
    (hminor : x ∉ ThreePrimeAnalysis.majorArcUnion ⌊R⌋₊ (2 * R / X)) :
    ∃ a : ℤ, ∃ q : ℕ, R ≤ (q : ℝ) ∧ (q : ℝ) ≤ X / R ∧ 0 < q ∧
      IsCoprime a (q : ℤ) ∧ |x - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion