OAI/NumberTheory/Ostmann/Tree/PairSquareMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.fieldPairCoefficientMoment line 14
2. theorem OAI.Ostmann.fieldPairCoefficientMoment_zero line 18
3. theorem OAI.Ostmann.sum_fieldPairCoefficientMoment line 23
4. theorem OAI.Ostmann.mellinCoefficient_mul_const line 29
5. theorem OAI.Ostmann.fieldPair_scaled_square_coefficient_le line 40

   Source documentation

   Multiplication by the difference can be absorbed into the fixed square coset; the zero difference is handled by the zero extension.

   theorem fieldPair_scaled_square_coefficient_le {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (d : ZMod p) (K : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
       ‖mellinCoefficient (fun r : (ZMod p)ˣ =>
         fieldBottomPairValue g d ((K : ZMod p) * d * (r : ZMod p) ^ 2)) ρ‖ ^ 2 ≤
         2 * squareCharacterMass (fun χ => fieldPairCoefficientMoment g χ d) ρ := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.fieldBottomPairValue, OAI.Ostmann.squareCharacterMass, OAI.Ostmann.fieldPairCoefficientMoment

6. theorem OAI.Ostmann.fieldPair_scaled_square_mean_le line 56
7. theorem OAI.Ostmann.samePair_fixed_arguments_le line 73

   Source documentation

   First average the held pair's split, while the two pair differences remain fixed. This costs two square fibers and the moving-pair coefficient.

   theorem samePair_fixed_arguments_le {p : ℕ} [Fact p.Prime]
       (g h : ZMod p → ℂ) (d e : ZMod p) (K L : (ZMod p)ˣ)
       (ρ : MulChar (ZMod p) ℂ) :
       (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ b : (ZMod p)ˣ,
         ‖mellinCoefficient (fun r : (ZMod p)ˣ =>
           fieldBottomPairValue g d ((K : ZMod p) * d * (r : ZMod p) ^ 2) *
           fieldBottomPairValue h e ((L : ZMod p) * e * (b : ZMod p) ^ 2)) ρ‖ ^ 2) ≤
         4 * squareCharacterMass (fun χ => fieldPairCoefficientMoment g χ d) ρ *
           fieldPairMoment h e := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.fieldBottomPairValue, OAI.Ostmann.squareCharacterMass, OAI.Ostmann.fieldPairCoefficientMoment, OAI.Ostmann.fieldPairMoment