Vinogradov mean value theorem

vinogradov_mean_value

Submitter: Junyan Xu.

Notes: The Bourgain–Demeter–Guth proof relies solely on harmonic analysis techniques rather than number theoretic methods all previous progress relied on, and allows integers to be replaced with arbitrary well separated real numbers. The theorem is derived as a consequence of a sharp decoupling inequality for curves. Wooley's proof uses his nested efficient congruencing method, which in contrast with the l2-decoupling method makes no use of multilinear Kakeya estimates, so is of sufficient flexibility to be applicable in algebraic number fields, and in function fields.

Source: Unavailable.

Informal solution: Unavailable.

theorem declaration uses `sorry`vinogradov_mean_value (s k : ℕ) (ε : ℝ) (hε : 0 < ε) :
    LeanEval.NumberTheory.VinogradovMeanValue.J s k =O[Filter.atTop]
      fun X ↦ (X ^ (s + ε) + X ^ ((2 * s : ℝ) - k * (k + 1) / 2 + ε) : ℝ) := bys:ℕk:ℕε:ℝhε:0 < ε⊢ J s k =O[Filter.atTop] fun X => ↑X ^ (↑s + ε) + ↑X ^ (2 * ↑s - ↑k * (↑k + 1) / 2 + ε)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.