OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticCRTSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.crtSplitExternalEquiv line 12

   Source documentation

   Simultaneously split the integer and unit giant residues.

   noncomputable def crtSplitExternalEquiv (c r : ℕ) (hc : c.Coprime r) :
       (ZMod (c * r) × (ZMod (c * r))ˣ) ≃
         (ZMod c × (ZMod c)ˣ) × (ZMod r × (ZMod r)ˣ) :=
   …

2. theorem OAI.Ostmann.crt_external_regular_with_remainder line 20

   Source documentation

   The signed remainder includes spectator, internal-prime and frequency tests, including the retained Page correction. No absolute value is taken.

   theorem crt_external_regular_with_remainder {I : Type*} [Fintype I] [DecidableEq I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime] [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (r : ℕ) [NeZero r] [NeZero ((∏ i, p i) * r)]
       (hcop : (∏ i, p i).Coprime r)
       (active : I → Bool) (a : ∀ i, (ZMod (p i))ˣ) (g : ∀ i, ZMod (p i) → ℂ)
       (hg : ∀ i, g i 0 = 0) (henergy : ∀ i, (∑ x : ZMod (p i), ‖g i x‖ ^ 2) = p i)
       (F : ZMod r × (ZMod r)ˣ → ℂ) :
       (Fintype.card (ZMod ((∏ i, p i) * r) × (ZMod ((∏ i, p i) * r))ˣ) : ℂ)⁻¹ *
         (∑ z,
           ((∏ i, externalRegularLocal (active i) (a i) (g i)
             (crtExternalPairEquiv p hc (crtSplitExternalEquiv (∏ i, p i) r hcop z).1 i) : ℝ) : ℂ) *
   …

   Mentions: OAI.Ostmann.externalRegularLocal, OAI.Ostmann.crtExternalPairEquiv, OAI.Ostmann.crtSplitExternalEquiv