OAI/NumberTheory/TwoPoint/Fourier/MinorArcShiftedFiber.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A shifted additive fiber is bounded by the unshifted additive energy.

  1. def OAI.TwoPointCorrelations.minorArcValueCount line 13
  2. lemma OAI.TwoPointCorrelations.minor_arc_value_support line 16
  3. lemma OAI.TwoPointCorrelations.minor_arc_pair_fiber line 22
  4. lemma OAI.TwoPointCorrelations.minor_arc_shifted_value_squares line 47
  5. lemma OAI.TwoPointCorrelations.minor_arc_shifted_pair_card line 62
  6. theorem OAI.TwoPointCorrelations.minor_arc_prime_shifted_fiber line 83

    Source documentation

    Every difference-of-prime-sums fiber has size at most the zero fiber.

    theorem minor_arc_prime_shifted_fiber (P : Finset ℕ) (h : ℤ) :
    (((P ×ˢ P) ×ˢ (P ×ˢ P)).filter
      (fun v => ((v.1.1 : ℤ) + v.1.2) - ((v.2.1 : ℤ) + v.2.2) = h)).card ≤
      Finset.addEnergy P P := by
…