Vinogradov mean value theorem

Loading leaderboard data…

Problem statement

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 : ) (ε : ) ( : 0 < ε) : LeanEval.NumberTheory.VinogradovMeanValue.J s k =O[Filter.atTop] fun X (X ^ (s + ε) + X ^ ((2 * s : ) - k * (k + 1) / 2 + ε) : ) := s:k:ε::0 < εJ s k =O[Filter.atTop] fun X => X ^ (s + ε) + X ^ (2 * s - k * (k + 1) / 2 + ε) All goals completed! 🐙