OAI/NumberTheory/Ostmann/Characters/QuartetTotalMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quartetParameterValue_sum_characters line 16
2. theorem OAI.Ostmann.fieldPairMoment_parameter_average line 29
3. theorem OAI.Ostmann.quartet_pair_parameter_average line 46
4. def OAI.Ostmann.quartetParameterMoment line 73
5. theorem OAI.Ostmann.quartetParameterMoment_nonneg line 79
6. theorem OAI.Ostmann.sum_quartetParameterMoment line 86

   Source documentation

   The total local mass is exactly a nonnegative difference convolution.

   theorem sum_quartetParameterMoment {p : ℕ} [Fact p.Prime]
       (g h : ZMod p → ℂ) (left right : Bool) (y : (ZMod p)ˣ) :
       (∑ ν : MulChar (ZMod p) ℂ, quartetParameterMoment g h left right ν y) =
         (Fintype.card (ZMod p)ˣ : ℝ) / (p : ℝ) ^ 2 *
           differenceMoment (fieldPairMoment g) (fieldPairMoment h) y := by
   …

   Mentions: OAI.Ostmann.quartetParameterMoment, OAI.Ostmann.differenceMoment, OAI.Ostmann.fieldPairMoment

7. theorem OAI.Ostmann.quartetParameterMoment_total_mean_le line 132

   Source documentation

   Uniform bounded total mass, simultaneously for all four friendly/bad choices.

   theorem quartetParameterMoment_total_mean_le {p : ℕ} [Fact p.Prime]
       (g h : ZMod p → ℂ) (hg : g 0 = 0) (hh : h 0 = 0)
       (heg : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
       (heh : (∑ x : ZMod p, ‖h x‖ ^ 2) ≤ (p : ℝ)) (left right : Bool) :
       (∑ ν : MulChar (ZMod p) ℂ, (∑ y : (ZMod p)ˣ,
         quartetParameterMoment g h left right ν y) / (Fintype.card (ZMod p)ˣ : ℝ)) ≤
           ((p : ℝ) / (Fintype.card (ZMod p)ˣ : ℝ)) ^ 2 := by
   …

   Mentions: OAI.Ostmann.quartetParameterMoment