OAI/NumberTheory/EgyptianFractions/VaughanHyperbolicNearRational.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.VaughanBilinear.near_rational_hyperbolic_bilinear_sq_le line 14

   Source documentation

   A full Type-II estimate for the actual hyperbolic region m*n ≤ X. The rational approximation is the only analytic input: support intersection, geometric cancellation, harmonic spacing, and coefficient-energy estimates are all supplied by checked lemmas. Empty row and column intervals are allowed.

   theorem near_rational_hyperbolic_bilinear_sq_le
       (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (X L U V N : ℕ) (t : Finset ℕ)
       (ht : t ⊆ Finset.Ico V (V + N)) (hpos : ∀ n ∈ t, 0 < n)
       (c b : ℕ → ℂ) :
       ‖∑ m ∈ Finset.Icc L U, c m * ∑ n ∈ t,
         b n * HyperbolaCorrelation.column θ X n m‖ ^ 2 ≤
         (∑ m ∈ Finset.Icc L U, ‖c m‖ ^ 2) *
           ((2 * (N : ℝ) / q + 1) *
             (2 * ((U + 1 - L : ℕ) : ℝ) +
   …

   Mentions: OAI.Problem337.HyperbolaCorrelation.column