MajorArcApproximationBridge.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MinorArc.rationalWindow_eq_rationalArc line 10
Source documentation
The elementary finite-window radius agrees with the variable-radius API.
```
theorem rationalWindow_eq_rationalArc (N q a : ℕ) :
    rationalWindow N q a = ThreePrimeAnalysis.rationalArc q a (1 / (N : ℝ)) := by
…
```
Mentions: OAI.Problem337.MinorArc.rationalWindow, OAI.Problem337.ThreePrimeAnalysis.rationalArc
theorem OAI.Problem337.MinorArc.majorArcs_unit_subset_majorArcUnion line 16
Source documentation
Reduced Dirichlet neighborhoods on the unit interval are contained in exactly the finite major-arc union used by the integral error estimates.
```
theorem majorArcs_unit_subset_majorArcUnion {Q N : ℕ} (hN : 2 ≤ N) :
    majorArcs Q N ∩ Set.Icc (0 : ℝ) 1 ⊆
      ThreePrimeAnalysis.majorArcUnion Q (1 / (N : ℝ)) := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.ThreePrimeAnalysis.majorArcUnion
theorem OAI.Problem337.MinorArc.majorArcUnion_subset_majorArcs line 24
Source documentation
Removing reduction from the displayed major-arc centers does not enlarge the union beyond the reduced-rational Dirichlet major arcs.
```
theorem majorArcUnion_subset_majorArcs {Q N : ℕ} (hN : 0 < N) :
    ThreePrimeAnalysis.majorArcUnion Q (1 / (N : ℝ)) ⊆ majorArcs Q N := by
…
```
Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion, OAI.Problem337.MinorArc.majorArcs
theorem OAI.Problem337.MinorArc.majorArcs_unit_eq_majorArcUnion_unit line 47
Source documentation
The two major-arc conventions are identical after restricting to [0,1].
```
theorem majorArcs_unit_eq_majorArcUnion_unit {Q N : ℕ} (hN : 2 ≤ N) :
    majorArcs Q N ∩ Set.Icc (0 : ℝ) 1 =
      ThreePrimeAnalysis.majorArcUnion Q (1 / (N : ℝ)) ∩ Set.Icc (0 : ℝ) 1 := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

theorem OAI.Problem337.MinorArc.exists_minor_fraction_of_not_mem_majorArcUnion line 58

Source documentation

Outside the finite major arcs used for integration, Dirichlet gives an actual reduced approximation in the minor-arc denominator window.

theorem exists_minor_fraction_of_not_mem_majorArcUnion {Q N : ℕ}
    (hN : 2 ≤ N) {x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1)
    (hminor : x ∉ ThreePrimeAnalysis.majorArcUnion Q (1 / (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.ThreePrimeAnalysis.majorArcUnion