OAI/NumberTheory/Ostmann/Construction/GroupedPhaseFactorization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.groupedPivotProduct_pos line 12
2. theorem OAI.Ostmann.directedPrimePhase_factor_grouped line 18

   Source documentation

   All constituents are retained. The pivot row uses the single residue v/H modulo their product; the retained factor uses that product as an integer.

   theorem directedPrimePhase_factor_grouped {K I : Type*} [Fintype K] [Fintype I]
       (p : K ⊕ I → ℕ) [∀ j, Fact (p j).Prime]
       (χ : ∀ j, DirichletCharacter ℂ (p j))
       (t : ∀ j, ZMod (p j)) (ν : (K ⊕ I) → ℂ)
       (g : (K ⊕ I) → (K ⊕ I) → ℤ) (b : Option I → Option I → ℤ)
       (κ : K → ℂ) (ε : K → ℤ) (H Y : ℕ) (v : ℤ)
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (hHY : (∏ i, p (.inr i)) = H * Y)
       (hv : ∀ k, (v : ZMod (p (.inl k))) ≠ 0)
       (hν : ∀ k, ν (.inl k) = κ k * χ (.inl k) (v : ZMod (p (.inl k))) ^ (-ε k))
       (hself : ∀ k, g (.inl k) (.inl k) = 0)
       (hrow : ∀ k j, j ≠ .inl k → g (.inl k) j = ε k)
   …