OAI/NumberTheory/TwoPoint/Halasz/HalaszSparseCofactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The proved integer kernel attached to actual reciprocal-count cofactors.

  1. def OAI.TwoPointCorrelations.halaszSparseKernelError line 12
  2. lemma OAI.TwoPointCorrelations.halasz_triangle_dyadic_member line 16
  3. lemma OAI.TwoPointCorrelations.halasz_integer_kernel_on_samples line 29
  4. theorem OAI.TwoPointCorrelations.halasz_sparse_cofactor_energy line 46

    Source documentation

    An unconditional sparse mean square for the literal cofactor window.

    theorem halasz_sparse_cofactor_energy (P : Finset ℕ) (F : ℕ → ℂ)
    (hF : OneBounded F) (N : ℕ) {a : ℝ} (ha : 1 ≤ a)
    (hx : 2 ≤ (N:ℝ)/a) {T : ℝ} (hT : 0 ≤ T)
    (S : Finset ℝ) (hS : ∀ t ∈ S, |t| ≤ T)
    (hsep : ∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) :
    (∑ t ∈ S, ‖mrtCofactorPolynomial P F N a t‖^2) ≤
      (148800*((N:ℝ)/a)+(S.card:ℝ)*halaszSparseKernelError ((N:ℝ)/a) T)*(2*a/N) := by
…

    Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtCofactorPolynomial, OAI.TwoPointCorrelations.halaszSparseKernelError