OAI/NumberTheory/Ostmann/Characters/QuartetSpectrumBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two-bad quartet estimate in terms of its spectra

The hypotheses are the nonnegative spectrum bounds src40. This combines the previously proved Gauss fourth moment with all principal corrections.

  1. theorem OAI.Ostmann.norm_at_zero_le_spectrum_mass line 22
  2. theorem OAI.Ostmann.principal_fourier_norm_sq_le line 31
  3. theorem OAI.Ostmann.character_spectrum_energy_le line 49
  4. theorem OAI.Ostmann.two_bad_spectrum_sum_le line 59

    Source documentation

    Complete bound for the two-bad row of tree-twisted-convolution.

    theorem two_bad_spectrum_sum_le {p : ℕ} [Fact p.Prime]
    (f g : MulChar (ZMod p) ℂ → ZMod p → ℂ)
    (w v : MulChar (ZMod p) ℂ → ZMod p → ℝ)
    (hf : ∀ χ a, additiveFourier (f χ) a = (w χ a : ℂ))
    (hg : ∀ χ a, additiveFourier (g χ) a = (v χ a : ℂ))
    (hw : ∀ χ a, 0 ≤ w χ a) (hv : ∀ χ a, 0 ≤ v χ a)
    (J W R S : ℝ) (hR : 0 ≤ R)
    (hwmass : ∀ χ, (∑ a : ZMod p, w χ a) ≤ J)
    (hvmass : ∀ χ, (∑ a : ZMod p, v χ a) ≤ J)
    (hwmax : ∀ χ a, w χ a ≤ W)
    (hwr : ∀ χ, (∑ a : ZMod p, w χ a ^ 2) ≤ R)
    (hvr : ∀ χ, (∑ a : ZMod p, v χ a ^ 2) ≤ R)
…

    Mentions: OAI.Ostmann.additiveFourier