OAI/NumberTheory/Ostmann/Characters/QuartetHorizontalMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.rationalCutCharacterSum line 15
2. theorem OAI.Ostmann.rationalCutCharacterSum_mean_le line 32

   Source documentation

   Apply horizontal density first, then eliminate one surviving character. The majorants may vary with the quartet label but not with ancestor data.

   theorem rationalCutCharacterSum_mean_le {p : ℕ} [Fact p.Prime]
       (D : (ZMod p)ˣ) (n : ℕ) {C : (ZMod p)ˣ}
       (T : RationalTreeData (ZMod p)ˣ (n + 2) C) (XL XR : (ZMod p)ˣ)
       (c : TreeLeafTuple Bool (n + 2))
       (B : TreeLeafIndex n → MulChar (ZMod p) ℂ → ZMod p → ℝ)
       (sign : TreeLeafIndex n → ℤ) (i : TreeLeafIndex n)
       (hi : sign i = 1 ∨ sign i = -1) (M H : ℝ) (hM : 0 ≤ M)
       (hB : ∀ j χ y, 0 ≤ B j χ y)
       (hsmall : ∀ χ, (∑ y : (ZMod p)ˣ, B i χ y) / (Fintype.card (ZMod p)ˣ : ℝ) ≤ M)
       (hmass : ∀ j, (∑ χ : MulChar (ZMod p) ℂ,
         (∑ y : (ZMod p)ˣ, B j χ y) / (Fintype.card (ZMod p)ˣ : ℝ)) ≤ H) :
       (∑ P : TreeLeafTuple (ZMod p)ˣ n, rationalCutCharacterSum D n T XL XR c B sign P) /
   …

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