VaughanBilinear.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.VaughanBilinear.energy_identity line 11

Source documentation

The exact correlation expansion of a weighted finite bilinear energy. No distinctness or unit-modulus assumption on the phase is needed.

theorem energy_identity {α β : Type*} (s : Finset α) (t : Finset β)
    (b : β → ℂ) (z : α → β → ℂ) :
    ((∑ m ∈ s, ‖∑ n ∈ t, b n * z m n‖ ^ 2 : ℝ) : ℂ) =
      ∑ n ∈ t, ∑ k ∈ t, b n * (starRingEnd ℂ) (b k) *
        ∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k) := by
…

theorem OAI.Problem337.VaughanBilinear.energy_le_correlations line 42

Source documentation

Bounding a bilinear energy by absolute correlations retains the arithmetic cancellation in the first variable.

theorem energy_le_correlations {α β : Type*} (s : Finset α) (t : Finset β)
    (b : β → ℂ) (z : α → β → ℂ) :
    (∑ m ∈ s, ‖∑ n ∈ t, b n * z m n‖ ^ 2) ≤
      ∑ n ∈ t, ∑ k ∈ t, ‖b n‖ * ‖b k‖ *
        ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖ := by
…

theorem OAI.Problem337.VaughanBilinear.norm_bilinear_sq_le line 61

Source documentation

Finite Type-II Cauchy--Schwarz, with the full correlation sum explicit. This is an unconditional algebraic bound, not a minor-arc hypothesis.

theorem norm_bilinear_sq_le {α β : Type*} (s : Finset α) (t : Finset β)
    (a : α → ℂ) (b : β → ℂ) (z : α → β → ℂ) :
    ‖∑ m ∈ s, a m * ∑ n ∈ t, b n * z m n‖ ^ 2 ≤
      (∑ m ∈ s, ‖a m‖ ^ 2) *
        (∑ n ∈ t, ∑ k ∈ t, ‖b n‖ * ‖b k‖ *
          ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖) := by
…

theorem OAI.Problem337.VaughanBilinear.diagonal_correlation line 79

Source documentation

For unit phases the diagonal correlation is exactly the number of rows.

theorem diagonal_correlation {α β : Type*} (s : Finset α)
    (z : α → β → ℂ) (n : β) (hz : ∀ m ∈ s, ‖z m n‖ = 1) :
    ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m n)‖ = (s.card : ℝ) := by
…

theorem OAI.Problem337.VaughanBilinear.correlation_sum_split line 94

Source documentation

Exact diagonal/off-diagonal separation; erased indices do not count a diagonal pair twice, including when either indexing set is empty.

theorem correlation_sum_split {α β : Type*} [DecidableEq β]
    (s : Finset α) (t : Finset β) (z : α → β → ℂ)
    (hz : ∀ m ∈ s, ∀ n ∈ t, ‖z m n‖ = 1) :
    (∑ n ∈ t, ∑ k ∈ t, ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖) =
      (s.card : ℝ) * t.card +
        ∑ n ∈ t, ∑ k ∈ t.erase n,
          ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖ := by
…

theorem OAI.Problem337.VaughanBilinear.norm_bilinear_sq_le_offDiagonal line 117

Source documentation

Bounded coefficient version of Type-II Cauchy--Schwarz. The diagonal is evaluated exactly; only genuine off-diagonal correlations remain.

theorem norm_bilinear_sq_le_offDiagonal {α β : Type*} [DecidableEq β]
    (s : Finset α) (t : Finset β) (a : α → ℂ) (b : β → ℂ)
    (z : α → β → ℂ) (B : ℝ) (hB : 0 ≤ B)
    (hb : ∀ n ∈ t, ‖b n‖ ≤ B)
    (hz : ∀ m ∈ s, ∀ n ∈ t, ‖z m n‖ = 1) :
    ‖∑ m ∈ s, a m * ∑ n ∈ t, b n * z m n‖ ^ 2 ≤
      (∑ m ∈ s, ‖a m‖ ^ 2) * B ^ 2 *
        ((s.card : ℝ) * t.card + ∑ n ∈ t, ∑ k ∈ t.erase n,
          ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖) := by
…

def OAI.Problem337.VaughanBilinear.phase line 147
Source documentation
The standard real additive phase, with the 2π convention.
```
def phase (x : ℝ) : ℂ := Real.fourierChar x
```
theorem OAI.Problem337.VaughanBilinear.norm_phase line 149
theorem OAI.Problem337.VaughanBilinear.phase_mul_conj line 151
theorem OAI.Problem337.VaughanBilinear.phase_nat_mul line 157
theorem OAI.Problem337.VaughanBilinear.phase_sum_mul_bound line 162
Source documentation
An exact geometric cancellation bound in a form valid even at resonance.
```
theorem phase_sum_mul_bound (x : ℝ) (M : ℕ) :
    ‖∑ m ∈ Finset.range M, phase (x * m)‖ * ‖1 - phase x‖ ≤ 2 := by
…
```
Mentions: OAI.Problem337.VaughanBilinear.phase
theorem OAI.Problem337.VaughanBilinear.phase_sum_le_min line 171
Source documentation
The usual geometric sum bound away from resonance.
```
theorem phase_sum_le_min (x : ℝ) (M : ℕ) (hx : phase x ≠ 1) :
    ‖∑ m ∈ Finset.range M, phase (x * m)‖ ≤
      min (M : ℝ) (2 / ‖1 - phase x‖) := by
…
```
Mentions: OAI.Problem337.VaughanBilinear.phase
def OAI.Problem337.VaughanBilinear.geometricBound line 183
Source documentation
A total geometric majorant. Resonant frequencies use the trivial bound; the definition never interprets division by zero as cancellation.
```
def geometricBound (M : ℕ) (x : ℝ) : ℝ :=
…
```
theorem OAI.Problem337.VaughanBilinear.phase_sum_le_geometricBound line 186

theorem OAI.Problem337.VaughanBilinear.real_phase_bilinear_sq_le line 197

Source documentation

The finite Type-II estimate specialized to a real bilinear phase. All remaining terms are explicit one-dimensional geometric sums, bounded without any Diophantine approximation assumption.

theorem real_phase_bilinear_sq_le (M : ℕ) (t : Finset ℕ)
    (a b : ℕ → ℂ) (θ B : ℝ) (hB : 0 ≤ B)
    (hb : ∀ n ∈ t, ‖b n‖ ≤ B) :
    ‖∑ m ∈ Finset.range M, a m * ∑ n ∈ t, b n * phase (θ * m * n)‖ ^ 2 ≤
      (∑ m ∈ Finset.range M, ‖a m‖ ^ 2) * B ^ 2 *
        ((M : ℝ) * t.card + ∑ n ∈ t, ∑ k ∈ t.erase n,
          geometricBound M (θ * ((n : ℝ) - k))) := by
…

Mentions: OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.VaughanBilinear.geometricBound

theorem OAI.Problem337.VaughanBilinear.symmetric_weighted_sum_le line 229

Source documentation

A finite real Schur bound, proved by symmetrizing 2xy ≤ x²+y². The coefficients need not be nonnegative.

theorem symmetric_weighted_sum_le {β : Type*} (t : Finset β)
    (f : β → ℝ) (K : β → β → ℝ)
    (hK : ∀ n ∈ t, ∀ k ∈ t, 0 ≤ K n k)
    (hsym : ∀ n ∈ t, ∀ k ∈ t, K n k = K k n) :
    (∑ n ∈ t, ∑ k ∈ t, f n * f k * K n k) ≤
      ∑ n ∈ t, f n ^ 2 * ∑ k ∈ t, K n k := by
…

theorem OAI.Problem337.VaughanBilinear.correlation_norm_symm line 261

Source documentation

Reversing a correlation conjugates it, hence preserves its norm.

theorem correlation_norm_symm {α β : Type*} (s : Finset α)
    (z : α → β → ℂ) (n k : β) :
    ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖ =
      ‖∑ m ∈ s, z m k * (starRingEnd ℂ) (z m n)‖ := by
…

theorem OAI.Problem337.VaughanBilinear.norm_bilinear_sq_le_energy line 276

Source documentation

Type-II energy bound using an absolute correlation row bound. Unlike the bounded-coefficient version, this retains both coefficient squared sums and therefore applies directly to divisor-coefficient second-moment estimates.

theorem norm_bilinear_sq_le_energy {α β : Type*} (s : Finset α) (t : Finset β)
    (a : α → ℂ) (b : β → ℂ) (z : α → β → ℂ) (C : ℝ)
    (hrow : ∀ n ∈ t,
      (∑ k ∈ t, ‖∑ m ∈ s, z m n * (starRingEnd ℂ) (z m k)‖) ≤ C) :
    ‖∑ m ∈ s, a m * ∑ n ∈ t, b n * z m n‖ ^ 2 ≤
      (∑ m ∈ s, ‖a m‖ ^ 2) * C * (∑ n ∈ t, ‖b n‖ ^ 2) := by
…