PeriodicMajorArcs.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.MinorArc.periodicArc line 10
Source documentation
A major arc with all integer translates retained. Restricting this set to a unit interval handles the arc crossing the endpoint zero without loss.
```
def periodicArc (N : ℕ) (r : ℚ) : Set ℝ :=
…
```
theorem OAI.Problem337.MinorArc.mem_periodicArc_iff line 13
theorem OAI.Problem337.MinorArc.normalized_centers_translate_ne line 21
Source documentation
Normalized rational centers remain different under every pair of integer translates. This is where the half-open convention at the unit endpoints matters.
```
theorem normalized_centers_translate_ne {r s : ℚ}
    (hr : r ∈ Set.Ico (0 : ℚ) 1) (hs : s ∈ Set.Ico (0 : ℚ) 1)
    (hrs : r ≠ s) (k l : ℤ) : r + k ≠ s + l := by
…
```

theorem OAI.Problem337.MinorArc.periodic_rational_separation line 31

Source documentation

Reciprocal-product separation on the circle, not merely on the real line.

theorem periodic_rational_separation {r s : ℚ}
    (hr : r ∈ Set.Ico (0 : ℚ) 1) (hs : s ∈ Set.Ico (0 : ℚ) 1)
    (hrs : r ≠ s) (k : ℤ) :
    1 / ((r.den : ℝ) * s.den) ≤ |(r : ℝ) - s - k| := by
…

theorem OAI.Problem337.MinorArc.periodicArc_disjoint line 43
Source documentation
The canonical real-line disjointness theorem also gives disjoint periodic arcs, provided the normalized centers are different.
```
theorem periodicArc_disjoint {r s : ℚ}
    (hr : r ∈ Set.Ico (0 : ℚ) 1) (hs : s ∈ Set.Ico (0 : ℚ) 1)
    (hrs : r ≠ s) {N : ℕ} (hN : r.den + s.den < N) :
    Disjoint (periodicArc N r) (periodicArc N s) := by
…
```
Mentions: OAI.Problem337.MinorArc.periodicArc

theorem OAI.Problem337.MinorArc.periodic_major_arc_unique line 55

Source documentation

Every point has at most one normalized major-arc center in the usual 2Q < N disjointness window, including points near the unit endpoints.

theorem periodic_major_arc_unique {Q N : ℕ} (hQN : 2 * Q < N) {x : ℝ}
    {r s : ℚ} (hr : r ∈ Set.Ico (0 : ℚ) 1) (hs : s ∈ Set.Ico (0 : ℚ) 1)
    (hrQ : r.den ≤ Q) (hsQ : s.den ≤ Q)
    (hxr : x ∈ periodicArc N r) (hxs : x ∈ periodicArc N s) : r = s := by
…

Mentions: OAI.Problem337.MinorArc.periodicArc

theorem OAI.Problem337.MinorArc.fract_den line 63
Source documentation
Integer translations preserve reduced denominator.
```
theorem fract_den (r : ℚ) : (Int.fract r).den = r.den := by
…
```
theorem OAI.Problem337.MinorArc.majorArcs_eq_normalized_periodic line 68
Source documentation
The all-rational major arcs have an exact normalized periodic presentation. In particular, no extra endpoint arc may be discarded at zero or one.
```
theorem majorArcs_eq_normalized_periodic (Q N : ℕ) :
    majorArcs Q N =
      {x | ∃ r : ℚ, r ∈ Set.Ico (0 : ℚ) 1 ∧ r.den ≤ Q ∧ x ∈ periodicArc N r} := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.periodicArc
theorem OAI.Problem337.MinorArc.measurableSet_periodicArc line 83
Source documentation
Periodic arcs are measurable countable unions of closed real intervals.
```
theorem measurableSet_periodicArc (N : ℕ) (r : ℚ) :
    MeasurableSet (periodicArc N r) := by
…
```
Mentions: OAI.Problem337.MinorArc.periodicArc
theorem OAI.Problem337.MinorArc.finite_normalized_centers line 95
Source documentation
Bounded-denominator, half-open normalized centers form a finite set.
```
theorem finite_normalized_centers (Q : ℕ) :
    {r : ℚ | r ∈ Set.Ico (0 : ℚ) 1 ∧ r.den ≤ Q}.Finite := by
…
```
def OAI.Problem337.MinorArc.normalizedCenters line 119
Source documentation
A finite, endpoint-safe index type for major-arc integration.
```
def normalizedCenters (Q : ℕ) : Finset ℚ :=
…
```
theorem OAI.Problem337.MinorArc.mem_normalizedCenters line 122
theorem OAI.Problem337.MinorArc.majorArcs_eq_iUnion_periodic line 127
Source documentation
Exact finite union, with the zero-center's wrap-around arc retained.
```
theorem majorArcs_eq_iUnion_periodic (Q N : ℕ) :
    majorArcs Q N = ⋃ r ∈ normalizedCenters Q, periodicArc N r := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.normalizedCenters, OAI.Problem337.MinorArc.periodicArc
theorem OAI.Problem337.MinorArc.pairwiseDisjoint_periodicArcs line 136
Source documentation
The finite periodic presentation is pairwise disjoint in the standard major-arc separation window.
```
theorem pairwiseDisjoint_periodicArcs {Q N : ℕ} (hQN : 2 * Q < N) :
    (normalizedCenters Q : Set ℚ).PairwiseDisjoint (periodicArc N) := by
…
```
Mentions: OAI.Problem337.MinorArc.normalizedCenters, OAI.Problem337.MinorArc.periodicArc