OAI/NumberTheory/Ostmann/Tree/SignedCycleBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_funSplitAt line 13
2. theorem OAI.Ostmann.signedCycleCoefficient_sum_le line 22

   Source documentation

   Once a cycle index has sign 1 or -1, its character is determined by all the others.

   theorem signedCycleCoefficient_sum_le {I G : Type*} [Fintype I] [DecidableEq I]
       [CommGroup G] [Fintype G] [DecidableEq G]
       (b : I → G → ℝ) (sign : I → ℤ) (i : I)
       (hi : sign i = 1 ∨ sign i = -1) (S : ℝ)
       (hb : ∀ j a, 0 ≤ b j a) (hS : ∀ a, b i a ≤ S) :
       (∑ ρ : I → G, if (∏ j : I, (ρ j) ^ sign j) = 1 then ∏ j : I, b j (ρ j) else 0) ≤
         S * ∏ j : {j : I // j ≠ i}, ∑ a : G, b j.1 a := by
   …

3. theorem OAI.Ostmann.cycleAverage_product_energy_le line 60

   Source documentation

   The quantitative form of the final cycle-projection step.

   theorem cycleAverage_product_energy_le {p : ℕ} [Fact p.Prime]
       {I : Type*} [Fintype I] [DecidableEq I]
       (f : I → (ZMod p)ˣ → ℂ) (sign : I → ℤ) (i : I)
       (hi : sign i = 1 ∨ sign i = -1) (S : ℝ)
       (hS : ∀ χ : MulChar (ZMod p) ℂ, ‖mellinCoefficient (f i) χ‖ ^ 2 ≤ S) :
       ((Fintype.card (ZMod p)ˣ : ℝ) ^ Fintype.card I)⁻¹ *
         (∑ m : I → (ZMod p)ˣ, ‖cycleAverage sign (fun m => ∏ j : I, f j (m j)) m‖ ^ 2) ≤
         S * ∏ j : {j : I // j ≠ i},
           (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * ∑ t : (ZMod p)ˣ, ‖f j.1 t‖ ^ 2 := by
   …

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