MinorArcMeasure.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MinorArc.isClosed_arc line 11
Source documentation
Each individual rational arc is closed.
```
theorem isClosed_arc (N : ℕ) (r : ℚ) : IsClosed (arc N r) := by
…
```
Mentions: OAI.Problem337.MinorArc.arc
theorem OAI.Problem337.MinorArc.measurableSet_majorArcs line 15
Source documentation
The major arcs form a measurable set, since the rational centers are countable.
```
theorem measurableSet_majorArcs (Q N : ℕ) : MeasurableSet (majorArcs Q N) := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs
def OAI.Problem337.MinorArc.rationalWindow line 24
Source documentation
A rational arc written without requiring its displayed fraction to be reduced.
```
def rationalWindow (N q a : ℕ) : Set ℝ :=
…
```
theorem OAI.Problem337.MinorArc.numerator_bounds_of_arc line 30
Source documentation
At scales at least two, a major arc meeting the unit interval has its reduced numerator between zero and its denominator.
```
theorem numerator_bounds_of_arc {N : ℕ} (hN : 2 ≤ N) {r : ℚ} {x : ℝ}
    (hx : x ∈ Set.Icc (0 : ℝ) 1) (hxr : x ∈ arc N r) :
    0 ≤ r.num ∧ r.num ≤ (r.den : ℤ) := by
…
```
Mentions: OAI.Problem337.MinorArc.arc
theorem OAI.Problem337.MinorArc.majorArcs_unit_subset line 61
Source documentation
An explicit finite cover, retaining the natural numerator and denominator needed to sum the arc lengths.
```
theorem majorArcs_unit_subset {Q N : ℕ} (hN : 2 ≤ N) :
    majorArcs Q N ∩ Set.Icc (0 : ℝ) 1 ⊆
      ⋃ q ∈ Finset.Icc 1 Q, ⋃ a ∈ Finset.range (q + 1), rationalWindow N q a := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.rationalWindow
theorem OAI.Problem337.MinorArc.volume_rationalWindow line 81
Source documentation
The length of one displayed rational window.
```
theorem volume_rationalWindow (N q a : ℕ) :
    volume (rationalWindow N q a) = ENNReal.ofReal (2 / ((q : ℝ) * N)) := by
…
```
Mentions: OAI.Problem337.MinorArc.rationalWindow
theorem OAI.Problem337.MinorArc.volume_windows_fixed_den_le line 88
Source documentation
The contribution from one positive denominator is at most 4/N.
```
theorem volume_windows_fixed_den_le (N q : ℕ) (hq : 1 ≤ q) :
    volume (⋃ a ∈ Finset.range (q + 1), rationalWindow N q a) ≤
      ENNReal.ofReal (4 / (N : ℝ)) := by
…
```
Mentions: OAI.Problem337.MinorArc.rationalWindow
theorem OAI.Problem337.MinorArc.volume_majorArcs_unit_le line 111
Source documentation
A quantitative major-arc volume bound on the unit interval. No prime distribution or exponential-sum estimate is used.
```
theorem volume_majorArcs_unit_le {Q N : ℕ} (hN : 2 ≤ N) :
    volume (majorArcs Q N ∩ Set.Icc (0 : ℝ) 1) ≤
      ENNReal.ofReal (4 * (Q : ℝ) / N) := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs
theorem OAI.Problem337.MinorArc.exists_unit_minor line 132
Source documentation
If 4Q < N, the major arcs do not cover the unit interval.
```
theorem exists_unit_minor {Q N : ℕ} (hN : 2 ≤ N) (hQN : 4 * Q < N) :
    ∃ x : ℝ, x ∈ Set.Icc (0 : ℝ) 1 ∧ x ∉ majorArcs Q N := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs