HyperbolaTypeII.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.HyperbolaCorrelation.phase_eq_vaughan line 11
lemma OAI.Problem337.HyperbolaCorrelation.phase_add line 13
theorem OAI.Problem337.HyperbolaCorrelation.phase_sum_Icc_le line 20
Source documentation
Translation of an integer interval does not affect its geometric-sum bound.
```
theorem phase_sum_Icc_le (x : ℝ) (L U : ℕ) :
    ‖∑ m ∈ Finset.Icc L U, phase (x * (m : ℝ))‖ ≤
      VaughanBilinear.geometricBound (U + 1 - L) x := by
…
```
Mentions: OAI.Problem337.HyperbolaCorrelation.phase, OAI.Problem337.VaughanBilinear.geometricBound
lemma OAI.Problem337.HyperbolaCorrelation.geometricBound_mono line 37
lemma OAI.Problem337.HyperbolaCorrelation.geometricBound_nonneg line 44
theorem OAI.Problem337.HyperbolaCorrelation.column_correlation_le line 51
Source documentation
A hyperbolic correlation admits the same geometric majorant as a full interval of rows. The moving endpoint introduces no additional loss.
```
theorem column_correlation_le (α : ℝ) (X L U n₁ n₂ : ℕ)
    (hn : 0 < max n₁ n₂) :
    ‖∑ m ∈ Finset.Icc L U, column α X n₁ m * conj (column α X n₂ m)‖ ≤
      VaughanBilinear.geometricBound (U + 1 - L) (α * ((n₁ : ℝ) - (n₂ : ℝ))) := by
…
```
Mentions: OAI.Problem337.HyperbolaCorrelation.column, OAI.Problem337.VaughanBilinear.geometricBound

theorem OAI.Problem337.HyperbolaCorrelation.norm_hyperbolic_bilinear_sq_le line 67

Source documentation

Type-II Cauchy--Schwarz for the actual region m*n ≤ X, with arbitrary complex coefficients and all correlations replaced by explicit geometric bounds.

theorem norm_hyperbolic_bilinear_sq_le (α : ℝ) (X L U : ℕ) (t : Finset ℕ)
    (a b : ℕ → ℂ) (ht : ∀ n ∈ t, 0 < n) :
    ‖∑ m ∈ Finset.Icc L U, a m * ∑ n ∈ t, b n * column α X n m‖ ^ 2 ≤
      (∑ m ∈ Finset.Icc L U, ‖a m‖ ^ 2) *
        (∑ n ∈ t, ∑ k ∈ t, ‖b n‖ * ‖b k‖ *
          VaughanBilinear.geometricBound (U + 1 - L) (α * ((n : ℝ) - (k : ℝ)))) := by
…

Mentions: OAI.Problem337.HyperbolaCorrelation.column, OAI.Problem337.VaughanBilinear.geometricBound

theorem OAI.Problem337.HyperbolaCorrelation.geometric_correlation_sum_split line 85

Source documentation

Separating the resonant diagonal in the geometric correlation majorant.

theorem geometric_correlation_sum_split (α : ℝ) (N : ℕ) (t : Finset ℕ) :
    (∑ n ∈ t, ∑ k ∈ t,
      VaughanBilinear.geometricBound N (α * ((n : ℝ) - (k : ℝ)))) =
      (N : ℝ) * t.card + ∑ n ∈ t, ∑ k ∈ t.erase n,
        VaughanBilinear.geometricBound N (α * ((n : ℝ) - (k : ℝ))) := by
…

Mentions: OAI.Problem337.VaughanBilinear.geometricBound

theorem OAI.Problem337.HyperbolaCorrelation.norm_hyperbolic_bilinear_sq_le_offDiagonal line 108

Source documentation

Bounded inner coefficients give a diagonal/off-diagonal Type-II estimate on a hyperbola with exactly the same row-length factor as the rectangular case.

theorem norm_hyperbolic_bilinear_sq_le_offDiagonal
    (α : ℝ) (X L U : ℕ) (t : Finset ℕ) (a b : ℕ → ℂ)
    (ht : ∀ n ∈ t, 0 < n) (B : ℝ) (hB : 0 ≤ B)
    (hb : ∀ n ∈ t, ‖b n‖ ≤ B) :
    ‖∑ m ∈ Finset.Icc L U, a m * ∑ n ∈ t, b n * column α X n m‖ ^ 2 ≤
      (∑ m ∈ Finset.Icc L U, ‖a m‖ ^ 2) * B ^ 2 *
        (((U + 1 - L : ℕ) : ℝ) * t.card + ∑ n ∈ t, ∑ k ∈ t.erase n,
          VaughanBilinear.geometricBound (U + 1 - L) (α * ((n : ℝ) - (k : ℝ)))) := by
…

Mentions: OAI.Problem337.HyperbolaCorrelation.column, OAI.Problem337.VaughanBilinear.geometricBound

theorem OAI.Problem337.HyperbolaCorrelation.norm_hyperbolic_bilinear_sq_le_energy line 137

Source documentation

A geometric row bound retains both coefficient energies for the actual hyperbolic region. The cutoff costs no extra factor in the Schur estimate.

theorem norm_hyperbolic_bilinear_sq_le_energy
    (α : ℝ) (X L U : ℕ) (t : Finset ℕ) (a b : ℕ → ℂ)
    (ht : ∀ n ∈ t, 0 < n) (C : ℝ)
    (hrow : ∀ n ∈ t, (∑ k ∈ t,
      VaughanBilinear.geometricBound (U + 1 - L) (α * ((n : ℝ) - (k : ℝ)))) ≤ C) :
    ‖∑ m ∈ Finset.Icc L U, a m * ∑ n ∈ t, b n * column α X n m‖ ^ 2 ≤
      (∑ m ∈ Finset.Icc L U, ‖a m‖ ^ 2) * C * (∑ n ∈ t, ‖b n‖ ^ 2) := by
…

Mentions: OAI.Problem337.VaughanBilinear.geometricBound, OAI.Problem337.HyperbolaCorrelation.column