OAI/NumberTheory/Ostmann/Tree/CrossPairHeldAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_square_coset_pair_le_four line 14
2. theorem OAI.Ostmann.crossPairMajorant_parameter_average line 30
3. theorem OAI.Ostmann.crossPair_held_coefficient_le line 44

   Source documentation

   Both held leaves may have any fixed square-coset multipliers. The moving coordinate multiplier may depend on both held leaves.

   theorem crossPair_held_coefficient_le {p : ℕ} [Fact p.Prime]
       (g h : ZMod p → ℂ) (left right : Bool) (y : (ZMod p)ˣ)
       (K L : (ZMod p)ˣ) (M : (ZMod p)ˣ → (ZMod p)ˣ → (ZMod p)ˣ)
       (ρ : MulChar (ZMod p) ℂ) :
       (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ a : (ZMod p)ˣ,
         (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * ∑ b : (ZMod p)ˣ,
           ‖mellinCoefficient (fun r => quartetRatioValue g h left right y
             (K * a ^ 2) (L * b ^ 2) (M a b * r ^ 2)) ρ‖ ^ 2) ≤
         8 * ((p : ℝ) / (Fintype.card (ZMod p)ˣ : ℝ)) ^ 2 *
           crossPairMajorant g h left right ρ⁻¹ y := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.crossPairMajorant