OAI/NumberTheory/Ostmann/Characters/SquareRatioCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.squareCharacterMass_inv line 15
2. theorem OAI.Ostmann.ratioTest_mellinCoefficient line 29
3. theorem OAI.Ostmann.ratioTest_square_mellin_bound line 44

   Source documentation

   The square-root ambiguity of a moving leaf costs exactly the square-fiber factor two. The ratio-to-difference normalization is explicit.

   theorem ratioTest_square_mellin_bound {p : ℕ} [Fact p.Prime]
       (F : ZMod p → ℂ) (y : (ZMod p)ˣ) (h0 : F 0 = 0) (hy : F y = 0)
       (K : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
       ‖mellinCoefficient (fun z => ratioTest F y (K * z ^ 2)) ρ‖ ^ 2 ≤
         2 * ((p : ℝ) / (Fintype.card (ZMod p)ˣ : ℝ)) ^ 2 *
           squareCharacterMass (fun ν => ‖ratioDifferenceTransform F y ν‖ ^ 2) ρ⁻¹ := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.ratioTest, OAI.Ostmann.squareCharacterMass, OAI.Ostmann.ratioDifferenceTransform

4. def OAI.Ostmann.quartetRatioValue line 68
5. theorem OAI.Ostmann.quartetRatioValue_at_difference line 75
6. theorem OAI.Ostmann.quartetRatioValue_square_mellin_bound line 97