OAI/NumberTheory/Ostmann/Construction/ExternalSquareFibers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.externalSquareFiberEquiv line 11
2. def OAI.Ostmann.externalSquareDecompose line 44
3. theorem OAI.Ostmann.externalSquare_average line 52

   Source documentation

   The original uniform mixed law first chooses its residues modulo p, then chooses uniformly among the p² lifts of that pair.

   theorem externalSquare_average (p : ℕ) [Fact p.Prime]
       (F : ZMod (p ^ 2) × (ZMod (p ^ 2))ˣ → ℂ) :
       (Fintype.card (ZMod (p ^ 2) × (ZMod (p ^ 2))ˣ) : ℂ)⁻¹ * (∑ z, F z) =
         (Fintype.card (ZMod p × (ZMod p)ˣ) : ℂ)⁻¹ *
           ∑ z : ZMod p × (ZMod p)ˣ, ((p : ℂ) ^ 2)⁻¹ *
             ∑ v : SquareLiftPairs p z.1 (z.2 : ZMod p),
               F ((externalSquareDecompose p).symm ⟨z, v⟩) := by
   …

   Mentions: OAI.Ostmann.SquareLiftPairs, OAI.Ostmann.externalSquareDecompose