MinorArcApproximation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.MinorArc.arc line 9
Source documentation
A closed major arc about a reduced rational, at Dirichlet scale N.
```
def arc (N : ℕ) (r : ℚ) : Set ℝ :=
…
```
def OAI.Problem337.MinorArc.majorArcs line 14
Source documentation
The union of major arcs with reduced denominator at most Q. The rational parameter retains coprimality without a separate hypothesis.
```
def majorArcs (Q N : ℕ) : Set ℝ :=
…
```
theorem OAI.Problem337.MinorArc.exists_dirichlet_approximation line 18
Source documentation
Dirichlet approximation supplies a reduced rational with bounded denominator.
```
theorem exists_dirichlet_approximation (x : ℝ) {N : ℕ} (hN : 0 < N) :
    ∃ r : ℚ, r.den ≤ N ∧ x ∈ arc N r := by
…
```
Mentions: OAI.Problem337.MinorArc.arc
theorem OAI.Problem337.MinorArc.exists_minor_approximation line 28
Source documentation
Outside the major arcs, Dirichlet's denominator is in the minor-arc window.
```
theorem exists_minor_approximation (x : ℝ) {Q N : ℕ} (hN : 0 < N)
    (hx : x ∉ majorArcs Q N) :
    ∃ r : ℚ, Q < r.den ∧ r.den ≤ N ∧ x ∈ arc N r := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.arc
theorem OAI.Problem337.MinorArc.arc_error_le_den_sq line 38
Source documentation
The Dirichlet error is also at most the reciprocal square of the reduced denominator, the form used by rational-approximation block estimates.
```
theorem arc_error_le_den_sq {N : ℕ} {r : ℚ} {x : ℝ}
    (hrN : r.den ≤ N) (hx : x ∈ arc N r) :
    |x - (r : ℝ)| ≤ 1 / (r.den : ℝ) ^ 2 := by
…
```
Mentions: OAI.Problem337.MinorArc.arc

theorem OAI.Problem337.MinorArc.exists_minor_coprime_fraction line 48

Source documentation

An explicit coprime numerator/denominator version of minor-arc extraction.

theorem exists_minor_coprime_fraction (x : ℝ) {Q N : ℕ} (hN : 0 < N)
    (hx : x ∉ majorArcs Q N) :
    ∃ a : ℤ, ∃ q : ℕ, Q < q ∧ q ≤ N ∧ 0 < q ∧
      IsCoprime a (q : ℤ) ∧
      |x - (a : ℝ) / q| ≤ 1 / ((q : ℝ) * N) ∧
      |x - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2 := by
…

Mentions: OAI.Problem337.MinorArc.majorArcs

theorem OAI.Problem337.MinorArc.rational_separation line 60
Source documentation
Distinct reduced rationals have the usual reciprocal-product separation.
```
theorem rational_separation {r s : ℚ} (hrs : r ≠ s) :
    1 / ((r.den : ℝ) * s.den) ≤ |(r : ℝ) - s| := by
…
```
theorem OAI.Problem337.MinorArc.arc_disjoint line 76
Source documentation
Two Dirichlet-scale major arcs cannot overlap when their denominator sum is smaller than the approximation scale.
```
theorem arc_disjoint {r s : ℚ} (hrs : r ≠ s) {N : ℕ}
    (hN : r.den + s.den < N) : Disjoint (arc N r) (arc N s) := by
…
```
Mentions: OAI.Problem337.MinorArc.arc

theorem OAI.Problem337.MinorArc.major_arc_unique line 96

Source documentation

In the standard window 2Q < N, all distinct major-arc centers are disjoint.

theorem major_arc_unique {Q N : ℕ} (hQN : 2 * Q < N) {x : ℝ}
    {r s : ℚ} (hr : r.den ≤ Q) (hs : s.den ≤ Q)
    (hxr : x ∈ arc N r) (hxs : x ∈ arc N s) : r = s := by
…

Mentions: OAI.Problem337.MinorArc.arc

theorem OAI.Problem337.MinorArc.rational_multiple_separation line 104
Source documentation
A nonintegral multiple of a reduced rational stays at least 1/q from any integer. This formulation is uniform in the chosen nearest integer.
```
theorem rational_multiple_separation (r : ℚ) (d k : ℤ)
    (hnd : ¬ (r.den : ℤ) ∣ d) :
    1 / (r.den : ℝ) ≤ |(r : ℝ) * d - k| := by
…
```

theorem OAI.Problem337.MinorArc.perturbed_multiple_separation line 125

Source documentation

Rational approximation remains separated from integers over a half-length block; this is the spacing input needed for irrational minor-arc block sums.

theorem perturbed_multiple_separation (r : ℚ) {x : ℝ} (d k : ℤ)
    (hx : |x - (r : ℝ)| ≤ 1 / (r.den : ℝ) ^ 2)
    (hnd : ¬ (r.den : ℤ) ∣ d)
    (hdsmall : |(d : ℝ)| ≤ (r.den : ℝ) / 2) :
    1 / (2 * (r.den : ℝ)) ≤ |x * d - k| := by
…

theorem OAI.Problem337.MinorArc.not_dvd_of_abs_lt line 144
Source documentation
A nonzero integer shorter than a positive modulus is not divisible by it.
```
theorem not_dvd_of_abs_lt {q : ℕ} {d : ℤ} (hd : d ≠ 0)
    (hlt : |(d : ℝ)| < (q : ℝ)) : ¬ (q : ℤ) ∣ d := by
…
```

theorem OAI.Problem337.MinorArc.perturbed_block_separation line 157

Source documentation

Distinct phases in a half-denominator block are uniformly separated modulo one, including after a Dirichlet-sized perturbation.

theorem perturbed_block_separation (r : ℚ) {x : ℝ} (m n k : ℤ)
    (hx : |x - (r : ℝ)| ≤ 1 / (r.den : ℝ) ^ 2)
    (hmn : m ≠ n) (hblock : |(m : ℝ) - n| ≤ (r.den : ℝ) / 2) :
    1 / (2 * (r.den : ℝ)) ≤ |x * m - x * n - k| := by
…

theorem OAI.Problem337.MinorArc.perturbed_block_round_separation line 170

Source documentation

The same separation in the nearest-integer distance convention.

theorem perturbed_block_round_separation (r : ℚ) {x : ℝ} (m n : ℤ)
    (hx : |x - (r : ℝ)| ≤ 1 / (r.den : ℝ) ^ 2)
    (hmn : m ≠ n) (hblock : |(m : ℝ) - n| ≤ (r.den : ℝ) / 2) :
    1 / (2 * (r.den : ℝ)) ≤
      |(x * m - x * n) - round (x * m - x * n)| := by
…