OAI/NumberTheory/Ostmann/Arithmetic/CRTLineAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.uniform_equiv_pi_average line 12
2. def OAI.Ostmann.crtUnitPairEquiv line 22
3. def OAI.Ostmann.crtExternalPairEquiv line 30
4. theorem OAI.Ostmann.crtUnitPairEquiv_apply line 38
5. theorem OAI.Ostmann.crtExternalPairEquiv_apply line 43
6. theorem OAI.Ostmann.crt_unit_pair_average line 49

   Source documentation

   The local line tests multiply when both giant coordinates are unit residues.

   theorem crt_unit_pair_average {I : Type*} [Fintype I] [DecidableEq I]
       (a : I → ℕ) [∀ i, NeZero (a i)] [NeZero (∏ i, a i)]
       (hc : Pairwise (fun i j => (a i).Coprime (a j)))
       (f : ∀ i, (ZMod (a i))ˣ × (ZMod (a i))ˣ → ℝ) :
       (Fintype.card ((ZMod (∏ i, a i))ˣ × (ZMod (∏ i, a i))ˣ) : ℝ)⁻¹ *
         (∑ z, ∏ i, f i (crtUnitPairEquiv a hc z i)) =
       ∏ i, (Fintype.card ((ZMod (a i))ˣ × (ZMod (a i))ˣ) : ℝ)⁻¹ * ∑ z, f i z :=
   …

   Mentions: OAI.Ostmann.crtUnitPairEquiv

7. theorem OAI.Ostmann.crt_external_pair_average line 59

   Source documentation

   The same exact factorization with the first giant an external integer.

   theorem crt_external_pair_average {I : Type*} [Fintype I] [DecidableEq I]
       (a : I → ℕ) [∀ i, NeZero (a i)] [NeZero (∏ i, a i)]
       (hc : Pairwise (fun i j => (a i).Coprime (a j)))
       (f : ∀ i, ZMod (a i) × (ZMod (a i))ˣ → ℝ) :
       (Fintype.card (ZMod (∏ i, a i) × (ZMod (∏ i, a i))ˣ) : ℝ)⁻¹ *
         (∑ z, ∏ i, f i (crtExternalPairEquiv a hc z i)) =
       ∏ i, (Fintype.card (ZMod (a i) × (ZMod (a i))ˣ) : ℝ)⁻¹ * ∑ z, f i z :=
   …

   Mentions: OAI.Ostmann.crtExternalPairEquiv