OAI/NumberTheory/TwoPoint/Halasz/HalaszSparseCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the integer-kernel error at the actual sparse-sample scale.

  1. def OAI.TwoPointCorrelations.halaszSparseErrorConstant line 10
  2. lemma OAI.TwoPointCorrelations.halasz_sparse_error_constant_pos line 13
  3. lemma OAI.TwoPointCorrelations.halasz_extra_cofactor_length line 18
  4. lemma OAI.TwoPointCorrelations.halasz_no_small_card_budget line 32
  5. lemma OAI.TwoPointCorrelations.halasz_sparse_error_exponential line 42
  6. theorem OAI.TwoPointCorrelations.halasz_sparse_sample_cost line 63
  7. theorem OAI.TwoPointCorrelations.halasz_sparse_cofactor_at_scale line 90

    Source documentation

    The sparse integer energy is uniformly bounded with the strict square-root margin supplied by the final original prime band.

    theorem halasz_sparse_cofactor_at_scale :
    ∀ᶠ L : ℝ in atTop, ∀ (P : Finset ℕ) (F : ℕ → ℂ), OneBounded F →
    ∀ (N : ℕ) (a T : ℝ), 1 ≤ a → 2 ≤ (N:ℝ)/a →
      Real.exp ((999/1000:ℝ)*L) ≤ (N:ℝ)/a → 0 ≤ T → T ≤ Real.exp L →
    ∀ S : Finset ℝ, (S.card:ℝ) ≤ Real.exp ((249/500:ℝ)*L) →
      (∀ t ∈ S, |t| ≤ T) →
      (∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) →
      (∑ t ∈ S, ‖mrtCofactorPolynomial P F N a t‖^2) ≤ 297602 := by
…

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