OAI/NumberTheory/Ostmann/Construction/ExternalSquareCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.externalSquareFiberEquiv_symm_values line 10
2. theorem OAI.Ostmann.externalSquareDecompose_symm_values line 18
3. theorem OAI.Ostmann.externalSquare_raw_average line 26

   Source documentation

   The disintegration formula with the two raw residue coordinates exposed.

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

   Mentions: OAI.Ostmann.SquareLiftPairs