OAI/NumberTheory/Ostmann/Construction/ExternalResidueReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.externalResidueReduction line 13
2. def OAI.Ostmann.primePairResidueReduction line 17
3. def OAI.Ostmann.externalReductionHom line 21
4. theorem OAI.Ostmann.externalReductionHom_surjective line 25
5. theorem OAI.Ostmann.uniform_external_residue_reduction line 35

   Source documentation

   Applies also to a prime-power modulus: all lifts have the same mass. The integrand may be signed or complex.

   theorem uniform_external_residue_reduction {m n : ℕ} [NeZero m] [NeZero n]
       (h : m ∣ n) (F : ZMod m × (ZMod m)ˣ → ℂ) :
       (Fintype.card (ZMod n × (ZMod n)ˣ) : ℂ)⁻¹ *
         (∑ z, F (externalResidueReduction h z)) =
       (Fintype.card (ZMod m × (ZMod m)ˣ) : ℂ)⁻¹ * ∑ z, F z := by
   …

   Mentions: OAI.Ostmann.externalResidueReduction

6. theorem OAI.Ostmann.uniform_prime_pair_residue_reduction line 53