OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowerSums.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Newton identities over the prime-power ring. The small integers in the identities are units when the prime exceeds the number of variables.

  1. lemma OAI.TwoPointCorrelations.halasz_unit_power_sums_esymm line 13
  2. theorem OAI.TwoPointCorrelations.halasz_unit_power_sums_product line 46
  3. theorem OAI.TwoPointCorrelations.halasz_prime_power_power_sums_product line 74
  4. theorem OAI.TwoPointCorrelations.halasz_prime_power_solution_mem line 84
  5. theorem OAI.TwoPointCorrelations.halasz_prime_power_solution_count line 97

    Source documentation

    A sufficient nonsingular congruence bound for the mean-value iteration. The factor k^k is deliberately used in place of the sharper k!.

    theorem halasz_prime_power_solution_count {p r k : ℕ} [Fact p.Prime]
    (hkp : k<p) (x : Fin k → ZMod (p^(r+1)))
    (hx : Function.Injective (fun i => halaszPrimePowerReduction p r (x i)))
    (F : Finset (Fin k → ZMod (p^(r+1))))
    (hF : ∀ y∈F, ∀ j : ℕ, 1≤j → j≤k → ∑ i, x i^j=∑ i, y i^j) :
    F.card ≤ k^k := by
…

    Mentions: OAI.TwoPointCorrelations.halaszPrimePowerReduction