RationalPhaseHyperbola.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.RationalPhaseSpacing.truncatedInv_mono_cap line 10
Source documentation
Monotonicity in the cap, valid also at integer phases.
```
theorem truncatedInv_mono_cap {Y Z : ℝ} (hYZ : Y ≤ Z) (x : ℝ) :
    truncatedInv Y x ≤ truncatedInv Z x := by
…
```
Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv

theorem OAI.Problem337.RationalPhaseSpacing.intDistance_lower_bound line 19

Source documentation

Positive indices in the first half-block cannot approach an integer more closely than 1/(2q). This removes the artificial singular term in Type I.

theorem intDistance_lower_bound
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (n : ℤ) (hn : n ≠ 0) (hsmall : 2 * |n| ≤ (q : ℤ)) :
    1 / (2 * (q : ℝ)) ≤ intDistance (α * n) := by
…

Mentions: OAI.Problem337.RationalPhaseSpacing.intDistance

theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_first_block_le line 30

Source documentation

First-block harmonic estimate with arbitrary, even varying, caps. The bound is independent of those caps because zero frequency is excluded.

theorem sum_truncatedInv_first_block_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (cap : ℤ → ℝ) :
    (∑ n ∈ Finset.Ico 1 ((q / 2 + 1 : ℕ) : ℤ),
      truncatedInv (cap n) (intDistance (α * n))) ≤
      8 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))) := by
…

Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_hyperbolic_block_le line 80

Source documentation

On later blocks the hyperbolic cap X/n is bounded by the cap at the left endpoint. This is the actual ingredient that removes an O(X) error.

theorem sum_truncatedInv_hyperbolic_block_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (L : ℤ) (hL : 0 < L) (X : ℝ) (hX : 0 ≤ X) :
    (∑ n ∈ Finset.Ico L (L + (q / 2 + 1 : ℕ)),
      truncatedInv (X / (n : ℝ)) (intDistance (α * n))) ≤
      2 * X / (L : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))) := by
…

Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_hyperbolic_prefix_blocks_le line 103

Source documentation

Prefix aggregation with hyperbolic caps. The first block has no singular term; the remaining singular terms sum harmonically rather than linearly.

theorem sum_truncatedInv_hyperbolic_prefix_blocks_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (X : ℝ) (hX : 0 ≤ X) (k : ℕ) :
    (∑ n ∈ Finset.Ico 1 ((k : ℤ) * (q / 2 + 1 : ℕ) + (q / 2 + 1 : ℕ)),
      truncatedInv (X / (n : ℝ)) (intDistance (α * n))) ≤
      ((k : ℝ) + 2) * (4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) +
        (2 * X / ((q / 2 + 1 : ℕ) : ℝ)) * (harmonic k : ℝ) := by
…

Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_hyperbolic_le line 162

Source documentation

A uniform hyperbolic reciprocal-distance bound. This is the scalar Type-I estimate: the potentially large cap contributes X/q, not X.

theorem sum_truncatedInv_hyperbolic_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (X : ℝ) (hX : 0 ≤ X) (M : ℕ) :
    (∑ n ∈ Finset.Icc 1 (M : ℤ),
      truncatedInv (X / (n : ℝ)) (intDistance (α * n))) ≤
      8 * ((M : ℝ) + q) * (1 + Real.log (2 * (q : ℝ))) +
        (4 * X / (q : ℝ)) * (1 + Real.log ((M : ℝ) + 1)) := by
…

Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance