RationalArcVolume.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ThreePrimeAnalysis.rationalArc line 11
Source documentation
A closed rational neighborhood of radius δ / q.
```
def rationalArc (q a : ℕ) (δ : ℝ) : Set ℝ :=
…
```
def OAI.Problem337.ThreePrimeAnalysis.majorArcUnion line 16
Source documentation
All rational neighborhoods with positive denominator at most Q and centers in [0,1]. Including nonreduced fractions only enlarges the set.
```
def majorArcUnion (Q : ℕ) (δ : ℝ) : Set ℝ :=
…
```
theorem OAI.Problem337.ThreePrimeAnalysis.measurableSet_majorArcUnion line 19
theorem OAI.Problem337.ThreePrimeAnalysis.volume_rationalArc line 24
theorem OAI.Problem337.ThreePrimeAnalysis.mem_rationalArc_iff line 30
theorem OAI.Problem337.ThreePrimeAnalysis.mem_majorArcUnion_iff line 35
theorem OAI.Problem337.ThreePrimeAnalysis.near_integer_fraction_mem_majorArcUnion line 45
Source documentation
For radii below one, an approximating rational to a point in [0,1] automatically has a numerator in [0,q]. Thus integer-indexed Dirichlet neighborhoods are covered by the finite union used in the volume estimate.
```
theorem near_integer_fraction_mem_majorArcUnion
    {Q q : ℕ} {a : ℤ} {δ x : ℝ} (hq : 0 < q) (hqQ : q ≤ Q)
    (hδ : δ < 1) (hx0 : 0 ≤ x) (hx1 : x ≤ 1)
    (hnear : |x - (a : ℝ) / q| ≤ δ / q) :
    x ∈ majorArcUnion Q δ := by
…
```
Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion
theorem OAI.Problem337.ThreePrimeAnalysis.volume_denominator_arcs_le line 78
Source documentation
Each fixed denominator contributes at most 4δ, without any coprimality or disjointness hypothesis.
```
theorem volume_denominator_arcs_le {q : ℕ} (hq : 1 ≤ q)
    {δ : ℝ} (hδ : 0 ≤ δ) :
    volume (⋃ a ∈ Finset.range (q + 1), rationalArc q a δ) ≤
      ENNReal.ofReal (4 * δ) := by
…
```
Mentions: OAI.Problem337.ThreePrimeAnalysis.rationalArc
theorem OAI.Problem337.ThreePrimeAnalysis.volume_majorArcUnion_le line 99
Source documentation
Total major-arc volume, valid even when the neighborhoods overlap.
```
theorem volume_majorArcUnion_le (Q : ℕ) {δ : ℝ} (hδ : 0 ≤ δ) :
    volume (majorArcUnion Q δ) ≤ ENNReal.ofReal (4 * (Q : ℝ) * δ) := by
…
```
Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion
theorem OAI.Problem337.ThreePrimeAnalysis.volume_unit_majorArcs_le line 116

theorem OAI.Problem337.ThreePrimeAnalysis.norm_integral_majorArcs_le line 123

Source documentation

Integrating any uniformly bounded error over a subset of the major arcs costs at most the elementary volume budget.

theorem norm_integral_majorArcs_le
    (Q : ℕ) {δ B : ℝ} (hδ : 0 ≤ δ) (hB : 0 ≤ B)
    {E : Set ℝ} (hE : E ⊆ majorArcUnion Q δ) (f : ℝ → ℂ)
    (hf : ∀ x ∈ E, ‖f x‖ ≤ B) :
    ‖∫ x in E, f x‖ ≤ B * (4 * (Q : ℝ) * δ) := by
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

theorem OAI.Problem337.ThreePrimeAnalysis.norm_cube_sub_cube_le line 138

Source documentation

A uniform cubic perturbation estimate for the major-arc approximation.

theorem norm_cube_sub_cube_le {z w : ℂ} {B ε : ℝ}
    (hB : 0 ≤ B) (hε : 0 ≤ ε) (hz : ‖z‖ ≤ B) (hw : ‖w‖ ≤ B)
    (hzw : ‖z - w‖ ≤ ε) : ‖z ^ 3 - w ^ 3‖ ≤ 3 * B ^ 2 * ε := by
…

theorem OAI.Problem337.ThreePrimeAnalysis.norm_integral_cubic_majorArc_error_le line 163

Source documentation

The major-arc cubic integral error has an explicit volume factor. This uses only pointwise approximation; it does not assert prime distribution.

theorem norm_integral_cubic_majorArc_error_le
    (Q : ℕ) {δ B ε : ℝ} (hδ : 0 ≤ δ) (hB : 0 ≤ B) (hε : 0 ≤ ε)
    {E : Set ℝ} (hE : E ⊆ majorArcUnion Q δ) (f g phase : ℝ → ℂ)
    (hf : ∀ x ∈ E, ‖f x‖ ≤ B) (hg : ∀ x ∈ E, ‖g x‖ ≤ B)
    (herr : ∀ x ∈ E, ‖f x - g x‖ ≤ ε)
    (hphase : ∀ x ∈ E, ‖phase x‖ ≤ 1) :
    ‖∫ x in E, (f x ^ 3 - g x ^ 3) * phase x‖ ≤
      12 * (Q : ℝ) * δ * B ^ 2 * ε := by
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion