OAI/NumberTheory/Ostmann/Characters/QuartetAllMajorants.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quartetOptionalMajorant line 15
2. theorem OAI.Ostmann.quartetOptionalMajorant_nonneg line 24
3. theorem OAI.Ostmann.quartetOptionalMajorant_total_mean_le line 38
4. theorem OAI.Ostmann.quartetOptional_cut_mean_le line 59

   Source documentation

   The horizontal sum includes every untouched quartet, and loses a small factor at any one quartet participating in the signed cycle.

   theorem quartetOptional_cut_mean_le {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (hg : g 0 = 0)
       (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
       (ε : ℝ) (hε : 0 ≤ ε) (hflat : MixedFourierBound g ε)
       (D : (ZMod p)ˣ) (n : ℕ) {C : (ZMod p)ˣ}
       (T : RationalTreeData (ZMod p)ˣ (n + 2) C) (XL XR : (ZMod p)ˣ)
       (c : TreeLeafTuple Bool (n + 2))
       (cL cR : TreeLeafIndex n → Bool) (choice : TreeLeafIndex n → Option QuartetMovingCase)
       (sign : TreeLeafIndex n → ℤ) (i : TreeLeafIndex n)
       (hi : sign i = 1 ∨ sign i = -1) (moving : QuartetMovingCase) (hmoving : choice i = some moving) :
       (∑ P : TreeLeafTuple (ZMod p)ˣ n,
         rationalCutCharacterSum D n T XL XR c
   …

   Mentions: OAI.Ostmann.MixedFourierBound, OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.QuartetMovingCase, OAI.Ostmann.rationalCutCharacterSum