OAI/NumberTheory/Ostmann/Characters/HeldCycleAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.uniform_product_average line 11
2. theorem OAI.Ostmann.held_cycle_product_energy line 26

   Source documentation

   Fubini and the cycle-character relation remain exact after exposing the independent held coordinates in every affected quartet.

   theorem held_cycle_product_energy {p : ℕ} [Fact p.Prime]
       {I H : Type*} [Fintype I] [DecidableEq I] [Fintype H]
       (f : I → H → (ZMod p)ˣ → ℂ) (sign : I → ℤ) :
       ((Fintype.card H : ℝ) ^ Fintype.card I)⁻¹ * (∑ h : I → H,
         ((Fintype.card (ZMod p)ˣ : ℝ) ^ Fintype.card I)⁻¹ *
           ∑ m : I → (ZMod p)ˣ,
             ‖cycleAverage sign (fun m => ∏ i : I, f i (h i) (m i)) m‖ ^ 2) =
       ∑ ρ : I → MulChar (ZMod p) ℂ,
         if (∏ i : I, (ρ i) ^ sign i) = 1 then
           ∏ i : I, (Fintype.card H : ℝ)⁻¹ * ∑ h : H, ‖mellinCoefficient (f i h) (ρ i)‖ ^ 2
         else 0 := by
   …

   Mentions: OAI.Ostmann.cycleAverage, OAI.Ostmann.mellinCoefficient

3. theorem OAI.Ostmann.held_cycle_product_energy_le line 50
4. theorem OAI.Ostmann.cycle_majorant_average line 72

   Source documentation

   Averaging independent quartet arguments factorizes each surviving character term before a single character is eliminated by the cycle.

   theorem cycle_majorant_average {I G Y : Type*} [Fintype I] [DecidableEq I] [Fintype G] [Fintype Y]
       [CommGroup G] [DecidableEq G] (B : I → G → Y → ℝ) (sign : I → ℤ) :
       ((Fintype.card Y : ℝ) ^ Fintype.card I)⁻¹ * (∑ y : I → Y,
         ∑ ρ : I → G, if (∏ i : I, (ρ i) ^ sign i) = 1 then ∏ i : I, B i (ρ i) (y i) else 0) =
       ∑ ρ : I → G, if (∏ i : I, (ρ i) ^ sign i) = 1 then
         ∏ i : I, (Fintype.card Y : ℝ)⁻¹ * ∑ y : Y, B i (ρ i) y else 0 := by
   …

5. theorem OAI.Ostmann.cycle_majorant_average_le line 89