OAI/NumberTheory/TwoPoint/Fourier/MinorArcBilinearWindow.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.minorArcBilinearWindow line 12
2. lemma OAI.TwoPointCorrelations.minor_arc_window_scalar line 17
3. lemma OAI.TwoPointCorrelations.minor_arc_bilinear_dual line 23
4. theorem OAI.TwoPointCorrelations.minor_arc_bilinear_fourth line 43

   Source documentation

   The full finite minor-arc inequality obtained by polarization, Hölder, geometric summation and the four-origin support estimate.

   theorem minor_arc_bilinear_fourth (P : Finset ℕ) (X M H d : ℕ) (hd : 0 < d)
       (hP : ∀ p ∈ P, 0 < p ∧ ∀ q ∈ P, q ≤ 2 * p)
       (a c : ℕ → ℂ) (ha : ∀ m ∈ range M, ‖a m‖ ≤ 1) (hc : ∀ p ∈ P, ‖c p‖ ≤ 1)
       (α V : ℝ) (hV : ∀ p ∈ P, (H : ℝ) / (d * p : ℕ) + 1 ≤ V) :
       (∑ k ∈ range X, ‖minorArcBilinearWindow P M H d a c α k‖) ^ 4 ≤
         (M : ℝ) ^ 3 * (X * (3 * H + 1) ^ 3 : ℕ) *
           ∑ p₁ ∈ P, ∑ p₂ ∈ P, ∑ p₃ ∈ P, ∑ p₄ ∈ P,
             minorArcGeometricBound V (α * ((p₁ : ℝ) + p₂ - p₃ - p₄)) := by
   …

   Mentions: OAI.TwoPointCorrelations.minorArcBilinearWindow, OAI.TwoPointCorrelations.minorArcGeometricBound