RationalArcErrorBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeAnalysis.norm_integral_cubic_majorArc_error_logbudget line 12

Source documentation

Explicit logarithmic budget for the cubic approximation error. A cutoff and radius of logarithmic size cost two powers of the logarithmic parameter.

theorem norm_integral_cubic_majorArc_error_logbudget
    {N C a b δ : ℝ} (Q : ℕ) (hN : 1 < N) (hC : 0 ≤ C) (hδ : 0 ≤ δ)
    (hQ : (Q : ℝ) ≤ (Real.log N) ^ b)
    (hδN : δ ≤ (Real.log N) ^ b / N)
    {E : Set ℝ} (hE : E ⊆ majorArcUnion Q δ) (f g phase : ℝ → ℂ)
    (hf : ∀ x ∈ E, ‖f x‖ ≤ C * N)
    (hg : ∀ x ∈ E, ‖g x‖ ≤ C * N)
    (herr : ∀ x ∈ E, ‖f x - g x‖ ≤ N / (Real.log N) ^ a)
    (hphase : ∀ x ∈ E, ‖phase x‖ ≤ 1) :
    ‖∫ x in E, (f x ^ 3 - g x ^ 3) * phase x‖ ≤
      12 * C ^ 2 * N ^ 2 * (Real.log N) ^ (2 * b - a) := by
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

theorem OAI.Problem337.ThreePrimeAnalysis.tendsto_majorArc_log_error_factor line 44
Source documentation
The logarithmic major-arc error factor tends to zero whenever the approximation saves more than twice the logarithmic cutoff exponent.
```
theorem tendsto_majorArc_log_error_factor (C a b : ℝ) (hab : 2 * b < a) :
    Tendsto (fun N : ℝ => 12 * C ^ 2 * (Real.log N) ^ (2 * b - a))
      atTop (𝓝 0) := by
…
```

theorem OAI.Problem337.ThreePrimeAnalysis.eventually_norm_integral_cubic_majorArc_error_le line 55

Source documentation

Uniform little-o form, with all arc sets and complex approximants quantified after the threshold. This consumes pointwise approximation estimates but does not assert any prime-distribution estimate.

theorem eventually_norm_integral_cubic_majorArc_error_le
    (C a b ε : ℝ) (hC : 0 ≤ C) (hab : 2 * b < a) (hε : 0 < ε) :
    ∀ᶠ N : ℝ in atTop, ∀ (Q : ℕ) (δ : ℝ), 0 ≤ δ →
      (Q : ℝ) ≤ (Real.log N) ^ b → δ ≤ (Real.log N) ^ b / N →
      ∀ (E : Set ℝ), E ⊆ majorArcUnion Q δ →
      ∀ (f g phase : ℝ → ℂ),
      (∀ x ∈ E, ‖f x‖ ≤ C * N) →
      (∀ x ∈ E, ‖g x‖ ≤ C * N) →
      (∀ x ∈ E, ‖f x - g x‖ ≤ N / (Real.log N) ^ a) →
      (∀ x ∈ E, ‖phase x‖ ≤ 1) →
      ‖∫ x in E, (f x ^ 3 - g x ^ 3) * phase x‖ ≤ ε * N ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

theorem OAI.Problem337.ThreePrimeAnalysis.cubic_majorArc_error_isLittleO line 79

Source documentation

Function-valued little-o conclusion for a moving major-arc set. The complex integral error is negligible compared with the quadratic main-term scale.

theorem cubic_majorArc_error_isLittleO
    (C a b : ℝ) (hC : 0 ≤ C) (hab : 2 * b < a)
    (Q : ℝ → ℕ) (δ : ℝ → ℝ) (E : ℝ → Set ℝ)
    (f g phase : ℝ → ℝ → ℂ)
    (hwindow : ∀ᶠ N : ℝ in atTop,
      0 ≤ δ N ∧ (Q N : ℝ) ≤ (Real.log N) ^ b ∧
      δ N ≤ (Real.log N) ^ b / N ∧ E N ⊆ majorArcUnion (Q N) (δ N) ∧
      (∀ x ∈ E N, ‖f N x‖ ≤ C * N) ∧
      (∀ x ∈ E N, ‖g N x‖ ≤ C * N) ∧
      (∀ x ∈ E N, ‖f N x - g N x‖ ≤ N / (Real.log N) ^ a) ∧
      (∀ x ∈ E N, ‖phase N x‖ ≤ 1)) :
    (fun N : ℝ => ∫ x in E N, (f N x ^ 3 - g N x ^ 3) * phase N x)
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion