VaughanNearRational.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.VaughanBilinear.phase_int line 11
theorem OAI.Problem337.VaughanBilinear.phase_fract line 19
theorem OAI.Problem337.VaughanBilinear.phase_eq_geometric_phase line 23
theorem OAI.Problem337.VaughanBilinear.phase_sum_le_truncatedInv line 31
Source documentation
The usual truncated reciprocal-distance majorant for a real geometric sum. Integer phases use the length cap, never a spurious zero reciprocal.
```
theorem phase_sum_le_truncatedInv (x : ℝ) (M : ℕ) :
    ‖∑ m ∈ Finset.range M, phase (x * m)‖ ≤
      RationalPhaseSpacing.truncatedInv M (RationalPhaseSpacing.intDistance x) := by
…
```
Mentions: OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

theorem OAI.Problem337.VaughanBilinear.near_rational_correlation_row_le line 61

Source documentation

Rational approximation provides an actual Type-II correlation row bound on every short block of integer columns, uniformly in the chosen row.

theorem near_rational_correlation_row_le
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (M : ℕ) (t : Finset ℤ)
    (hspan : ∀ n ∈ t, ∀ k ∈ t, 2 * |n - k| ≤ (q : ℤ)) (n : ℤ) :
    (∑ k ∈ t, ‖∑ m ∈ Finset.range M,
      phase (θ * m * n) * (starRingEnd ℂ) (phase (θ * m * k))‖) ≤
      2 * (M : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))) := by
…

Mentions: OAI.Problem337.VaughanBilinear.phase

theorem OAI.Problem337.VaughanBilinear.near_rational_bilinear_sq_le line 108

Source documentation

A proved near-rational Type-II estimate with both coefficient energies. The only number-theoretic hypothesis is the stated reduced approximation; all correlation/spacing/cancellation estimates are discharged.

theorem near_rational_bilinear_sq_le
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (M : ℕ) (t : Finset ℤ)
    (hspan : ∀ n ∈ t, ∀ k ∈ t, 2 * |n - k| ≤ (q : ℤ))
    (c : ℕ → ℂ) (b : ℤ → ℂ) :
    ‖∑ m ∈ Finset.range M, c m * ∑ n ∈ t, b n * phase (θ * m * n)‖ ^ 2 ≤
      (∑ m ∈ Finset.range M, ‖c m‖ ^ 2) *
        (2 * (M : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) *
          (∑ n ∈ t, ‖b n‖ ^ 2) := by
…

Mentions: OAI.Problem337.VaughanBilinear.phase

theorem OAI.Problem337.VaughanBilinear.near_rational_interval_correlation_row_le line 125

Source documentation

Actual near-rational row cancellation on an arbitrary integer interval, also valid for any subset of that interval.

theorem near_rational_interval_correlation_row_le
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (M : ℕ) (t : Finset ℤ) (L : ℤ) (N : ℕ)
    (ht : t ⊆ Finset.Ico L (L + N)) (n : ℤ) :
    (∑ k ∈ t, ‖∑ m ∈ Finset.range M,
      phase (θ * m * n) * (starRingEnd ℂ) (phase (θ * m * k))‖) ≤
      (2 * (N : ℝ) / q + 1) *
        (2 * (M : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) := by
…

Mentions: OAI.Problem337.VaughanBilinear.phase

theorem OAI.Problem337.VaughanBilinear.near_rational_interval_bilinear_sq_le line 177

Source documentation

Full rectangular Type-II estimate from a reduced rational approximation. No spacing, correlation, or equidistribution estimate remains as a premise.

theorem near_rational_interval_bilinear_sq_le
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (M : ℕ) (t : Finset ℤ) (L : ℤ) (N : ℕ)
    (ht : t ⊆ Finset.Ico L (L + N)) (c : ℕ → ℂ) (b : ℤ → ℂ) :
    ‖∑ m ∈ Finset.range M, c m * ∑ n ∈ t, b n * phase (θ * m * n)‖ ^ 2 ≤
      (∑ m ∈ Finset.range M, ‖c m‖ ^ 2) *
        ((2 * (N : ℝ) / q + 1) *
          (2 * (M : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))))) *
            (∑ n ∈ t, ‖b n‖ ^ 2) := by
…

Mentions: OAI.Problem337.VaughanBilinear.phase

theorem OAI.Problem337.VaughanBilinear.geometricBound_le_truncatedInv line 194
Source documentation
The explicit geometric majorant itself is bounded by the truncated reciprocal distance. This also allows variable inner interval lengths.
```
theorem geometricBound_le_truncatedInv (M : ℕ) (x : ℝ) :
    geometricBound M x ≤
      RationalPhaseSpacing.truncatedInv M (RationalPhaseSpacing.intDistance x) := by
…
```
Mentions: OAI.Problem337.VaughanBilinear.geometricBound, OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

theorem OAI.Problem337.VaughanBilinear.sum_geometricBound_difference_le line 226

Source documentation

A uniform harmonic row bound for indexed integer frequencies. The map into the interval must be injective, but need not exhaust the interval.

theorem sum_geometricBound_difference_le {β : Type*}
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (M : ℕ) (t : Finset β) (f : β → ℤ) (L : ℤ) (N : ℕ)
    (hf : ∀ k ∈ t, f k ∈ Finset.Ico L (L + N))
    (hinj : Set.InjOn f t) (n : ℤ) :
    (∑ k ∈ t, geometricBound M (θ * ((n - f k : ℤ) : ℝ))) ≤
      (2 * (N : ℝ) / q + 1) *
        (2 * (M : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) := by
…

Mentions: OAI.Problem337.VaughanBilinear.geometricBound