TwoBadFourier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Joining the four cases of the two-bad quartet sum

The nonprincipal part uses the fourth moment. The two cases with exactly one principal twist use its total energy and the other twist's maximum. The last case uses the principal maximum and a single energy bound.

theorem OAI.Ostmann.two_bad_nonprincipal_le line 24

Source documentation

A common fourth-moment bound controls all nonprincipal terms.

theorem two_bad_nonprincipal_le {p : ℕ} [Fact p.Prime]
    (F G : MulChar (ZMod p) ℂ → MulChar (ZMod p) ℂ → ZMod p → ℂ)
    (ν : MulChar (ZMod p) ℂ) (T : ℝ) (hT : 0 ≤ T)
    (hF : (∑ χ : MulChar (ZMod p) ℂ,
      ∑ α ∈ (Finset.univ : Finset (MulChar (ZMod p) ℂ)).erase 1,
        ∑ a : ZMod p, ‖F χ α a‖ ^ 4) ≤ T)
    (hG : (∑ ψ : MulChar (ZMod p) ℂ,
      ∑ β ∈ (Finset.univ : Finset (MulChar (ZMod p) ℂ)).erase 1,
        ∑ a : ZMod p, ‖G ψ β a‖ ^ 4) ≤ T) :
    (∑ χ : MulChar (ZMod p) ℂ, ∑ ψ : MulChar (ZMod p) ℂ, ∑ a : ZMod p,
      if ν * ψ⁻¹ ≠ 1 ∧ ν⁻¹ * χ⁻¹ ≠ 1 then
        ‖F χ (ν * ψ⁻¹) a‖ ^ 2 * ‖G ψ (ν⁻¹ * χ⁻¹) (-a)‖ ^ 2 else 0) ≤ T := by
…

theorem OAI.Ostmann.two_bad_fourier_sum_le line 46

Source documentation

The complete two-bad sum, including both principal-character exceptions.

theorem two_bad_fourier_sum_le {p : ℕ} [Fact p.Prime]
    (F G : MulChar (ZMod p) ℂ → MulChar (ZMod p) ℂ → ZMod p → ℂ)
    (ν : MulChar (ZMod p) ℂ) (T K M R S : ℝ)
    (hT : 0 ≤ T) (hK : 0 ≤ K) (hM : 0 ≤ M)
    (hF4 : (∑ χ : MulChar (ZMod p) ℂ,
      ∑ α ∈ (Finset.univ : Finset (MulChar (ZMod p) ℂ)).erase 1,
        ∑ a : ZMod p, ‖F χ α a‖ ^ 4) ≤ T)
    (hG4 : (∑ ψ : MulChar (ZMod p) ℂ,
      ∑ β ∈ (Finset.univ : Finset (MulChar (ZMod p) ℂ)).erase 1,
        ∑ a : ZMod p, ‖G ψ β a‖ ^ 4) ≤ T)
    (hFn : ∀ χ α, α ≠ 1 → ∀ a, ‖F χ α a‖ ^ 2 ≤ K)
    (hGn : ∀ ψ β, β ≠ 1 → ∀ a, ‖G ψ β a‖ ^ 2 ≤ K)
…