HalaszVinogradovDiagonal.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The diagonal algebra for the complete Vinogradov system: its first s power sums determine all elementary symmetric functions of s entries. This is the finite algebraic starting point for the mean-value argument underlying Ford's logarithmic exponential-sum estimate.

theorem OAI.TwoPointCorrelations.halasz_vinogradov_esymm line 17

theorem OAI.TwoPointCorrelations.halasz_vinogradov_multiset line 53

Source documentation

The complete diagonal system determines the multiset of its variables.

theorem halasz_vinogradov_multiset {s : ℕ} (x y : Fin s → ℚ)
    (hpower : ∀ j : ℕ, 1 ≤ j → j ≤ s → ∑ i, x i^j = ∑ i, y i^j) :
    (univ.val.map x) = (univ.val.map y) := by
…

def OAI.TwoPointCorrelations.halaszVinogradovFiber line 78
lemma OAI.TwoPointCorrelations.mem_halaszVinogradovFiber line 84
lemma OAI.TwoPointCorrelations.halasz_vinogradov_fiber_perm line 90
theorem OAI.TwoPointCorrelations.halasz_vinogradov_fiber_card line 116
def OAI.TwoPointCorrelations.halaszVinogradovCount line 133
theorem OAI.TwoPointCorrelations.halasz_vinogradov_diagonal_bound line 137
Source documentation
The diagonal-range upper bound for the complete Vinogradov system.
```
theorem halasz_vinogradov_diagonal_bound {s k N : ℕ} (hsk : s ≤ k) :
    halaszVinogradovCount s k N ≤ N^s*s.factorial := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszVinogradovCount
lemma OAI.TwoPointCorrelations.halasz_vinogradov_count_lower line 145
lemma OAI.TwoPointCorrelations.halasz_vinogradov_count_antitone line 156