RationalPhaseBlock.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The harmonic bound for one short rational phase block

theorem OAI.Ostmann.phase_bin_sum_eq line 13

theorem OAI.Ostmann.rational_phase_block_bound line 27

Source documentation

All points may be translated by an arbitrary integer block location. Only the pairwise short-shift condition enters the estimate.

theorem rational_phase_block_bound (θ : ℝ) (a : ℤ) (r N : ℕ) (M : ℕ → ℕ) (S : Finset ℕ)
    (hr : 0 < r) (hcop : a.natAbs.Coprime r)
    (happrox : |θ - (a : ℝ) / r| ≤ 1 / (r : ℝ) ^ 2)
    (hshort : ∀ i ∈ S, ∀ j ∈ S, 2 * |(((i : ℤ) - j : ℤ) : ℝ)| ≤ (r : ℝ))
    (hlen : ∀ h ∈ S, M h ≤ N) :
    ∑ h ∈ S, ‖∑ j ∈ Finset.range (M h), realAdditivePhase (θ * h) ^ j‖ ≤
      2 * ((N : ℝ) + r * (1 + Real.log r)) := by
…

Mentions: OAI.Ostmann.realAdditivePhase