OAI/NumberTheory/Ostmann/Construction/TransferCompletePhase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.retainedAdditiveBranch line 16
2. def OAI.Ostmann.retainedCharacterBranch line 22
3. def OAI.Ostmann.retainedPrimePhase line 32
4. theorem OAI.Ostmann.transfer_complete_phase line 44

   Source documentation

   This identifies the entire off-diagonal phase, after removal of the pivot's outgoing row. Its output is the actual directed graph update, with all additive cofactors and new unary factors included.

   theorem transfer_complete_phase {H Y : Type*} [Fintype H] [Fintype Y]
       (L R : H → ℕ) (U : Y → ℕ)
       [∀ h, Fact (L h).Prime] [∀ h, Fact (R h).Prime] [∀ y, Fact (U y).Prime]
       (t : ∀ p : ℕ, ZMod p)
       (χH : H → ∀ p : ℕ, DirichletCharacter ℂ p)
       (χY : Y → ∀ p : ℕ, DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
       (νL νR : H → ℂ) (νYL νYR : Y → ℂ) (M : ℕ) (v w s : ℤ)
       (hrel : v * (∏ h, R h) - w * (∏ h, L h) = s * M)
       (hc : Pairwise (fun i j => (transferredLabels L R U i).Coprime (transferredLabels L R U j)))
       (hM : ∀ i, M.Coprime (transferredLabels L R U i))
       (hs : ∀ i, IsUnit (s : ZMod (transferredLabels L R U i)))
   …

   Mentions: OAI.Ostmann.transferredLabels