TwistCauchy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Cauchy--Schwarz for the two-bad quartet twists

The two character changes are permutations. After excluding principal twists, the two squared energies are exactly the fourth-moment sums.

theorem OAI.Ostmann.sum_nonprincipal_twist line 22

theorem OAI.Ostmann.two_bad_twist_cauchy line 39

Source documentation

The nonprincipal part of the two-bad sum is controlled by two fourth moments.

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