OAI/NumberTheory/Ostmann/Characters/QuartetRatioSwap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quartetRatioValue_swap line 11
2. theorem OAI.Ostmann.samePair_right_held_coefficient_le line 35

   Source documentation

   The same-pair estimate on the right is the left estimate with the parent difference reversed and the product coordinate inverted.

   theorem samePair_right_held_coefficient_le {p : ℕ} [Fact p.Prime]
       (g h : ZMod p → ℂ) (y J K L : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
       (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ a : (ZMod p)ˣ,
         (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * ∑ b : (ZMod p)ˣ,
           ‖mellinCoefficient (fun r : (ZMod p)ˣ =>
             quartetRatioValue g h true true y (K * b ^ 2) (L * r ^ 2) (J * a ^ 2)) ρ‖ ^ 2) ≤
         8 * samePairMajorant (fieldPairCoefficientMoment h) (fieldPairMoment g) ρ (-y) := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.samePairMajorant, OAI.Ostmann.fieldPairCoefficientMoment, OAI.Ostmann.fieldPairMoment