VaughanRealTypeIHyperbolic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual near-rational estimates for the two Vaughan Type I terms

The prefix adapter uses the sharper canonical harmonic hyperbola bound for its scalar aggregation. The variable hyperbolic lengths are retained throughout. In particular the right hand side has size N / q + A + q, up to logarithmic factors, rather than the much larger fixed-cap estimate obtained by replacing every N / d with N.

theorem OAI.Problem337.VaughanHyperbolic.norm_phase_Ioc_mul_le_variable line 28
Source documentation
Every hyperbolic inner prefix has the required variable-cap envelope. This includes the zero-frequency case and does not require a nonresonance assumption.
```
theorem norm_phase_Ioc_mul_le_variable (α : ℝ) (N d k : ℕ) (hk : k ≤ N / d) :
    ‖∑ b ∈ Finset.Ioc 0 k, RealPhase.phase (α * (d * b : ℕ))‖ ≤
      truncatedInv ((N : ℝ) / d) (intDistance (α * d)) := by
…
```
Mentions: OAI.Problem337.RealPhase.phase

theorem OAI.Problem337.VaughanHyperbolic.sum_variable_reciprocal_Ioc_le line 45

Source documentation

The positive-initial-interval convention used by Vaughan's identity.

theorem sum_variable_reciprocal_Ioc_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (N A : ℕ) :
    (∑ d ∈ Finset.Ioc 0 A,
      truncatedInv ((N : ℝ) / d) (intDistance (α * d))) ≤
      RealTypeI.hyperbolicCost (N : ℝ) A q := by
…

Mentions: OAI.Problem337.RealTypeI.hyperbolicCost

theorem OAI.Problem337.VaughanHyperbolic.first_typeI_real_phase_bound line 76

Source documentation

The first actual Vaughan convolution, with its logarithmic inner weight, is bounded using only a reduced rational approximation to the frequency.

theorem first_typeI_real_phase_bound
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (N U : ℕ) :
    ‖weightedSum (Finset.Ioc 0 N) (fun n => RealPhase.phase (α * n))
        (shortPart U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log)‖ ≤
      2 * Real.log N * RealTypeI.hyperbolicCost (N : ℝ) (min U N) q := by
…

Mentions: OAI.Problem337.RealPhase.phase, OAI.Problem337.RealTypeI.hyperbolicCost

theorem OAI.Problem337.VaughanHyperbolic.second_typeI_real_phase_bound line 93

Source documentation

The second actual Vaughan convolution has one logarithmic coefficient factor and the same variable-length reciprocal budget.

theorem second_typeI_real_phase_bound
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (N U V : ℕ) :
    ‖weightedSum (Finset.Ioc 0 N) (fun n => RealPhase.phase (α * n))
        (typeICoefficient U V * ζ)‖ ≤
      Real.log N * RealTypeI.hyperbolicCost (N : ℝ) (min (U * V) N) q := by
…

Mentions: OAI.Problem337.RealPhase.phase, OAI.Problem337.RealTypeI.hyperbolicCost