MovingReducedCRT.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The original reduced arithmetic coefficient in the regular-prime CRT split

theorem OAI.Ostmann.crtSplitExternalEquiv_snd line 11
theorem OAI.Ostmann.movingReducedPairResidueCoefficient_modEq line 24

theorem OAI.Ostmann.periodic_coefficient_crt line 47

Source documentation

A periodic natural-coordinate coefficient descends to the second CRT coordinate without changing its signed value.

theorem periodic_coefficient_crt (C : ℕ → ℕ → ℂ) (c r : ℕ) [NeZero r] [NeZero (c * r)]
    (hcop : c.Coprime r)
    (hC : ∀ a b d e, Nat.ModEq r a d → Nat.ModEq r b e → C a b = C d e)
    (z : ZMod (c * r) × (ZMod (c * r))ˣ) :
    C z.1.val (z.2 : ZMod (c * r)).val =
      C (crtSplitExternalEquiv c r hcop z).2.1.val
        ((crtSplitExternalEquiv c r hcop z).2.2 : ZMod r).val := by
…

Mentions: OAI.Ostmann.crtSplitExternalEquiv

theorem OAI.Ostmann.periodic_coefficient_regular_average line 61

Source documentation

Both factors are evaluated at their original natural residue representatives. Only periodicity and the proved local transform energy are used in the split.

theorem periodic_coefficient_regular_average {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) (s : ℤ) (other : ∀ i, ZMod (p i))
    (hs : ∀ i, (s : ZMod (p i)) ≠ 0) (ho : ∀ i, other i ≠ 0)
    (g : ∀ i, ZMod (p i) → ℂ) (hg : ∀ i, g i 0 = 0)
    (henergy : ∀ i, (∑ x : ZMod (p i), ‖g i x‖ ^ 2) = p i)
    (C : ℕ → ℕ → ℂ)
    (hC : ∀ a b d e, Nat.ModEq r a d → Nat.ModEq r b e → C a b = C d e) :
    (Fintype.card (ZMod ((∏ i, p i) * r) × (ZMod ((∏ i, p i) * r))ˣ) : ℂ)⁻¹ *
      (∑ z : ZMod ((∏ i, p i) * r) × (ZMod ((∏ i, p i) * r))ˣ, (guardedRegularMultiplier p active s other g z.1.val
…

Mentions: OAI.Ostmann.guardedRegularMultiplier