GroupedPivotPhase.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing every constituent of a grouped pivot from the directed phase

theorem OAI.Ostmann.regular_prime_row_product line 13

Source documentation

A regular outgoing row includes the cofactor, with its diagonal omitted.

theorem regular_prime_row_product {I : Type*} [Fintype I] (p : I → ℕ)
    {q : ℕ} (χ : DirichletCharacter ℂ q) (b : I → I → ℤ) (i : I) (ε : ℤ)
    (hself : b i i = 0) (hrow : ∀ j, j ≠ i → b i j = ε) :
    (∏ j, χ (p j : ZMod q) ^ b i j) = χ (tupleCofactor p i : ZMod q) ^ ε := by
…

Mentions: OAI.Ostmann.tupleCofactor

theorem OAI.Ostmann.grouped_incoming_row line 25

Source documentation

The incoming exponents are constant over all prime constituents of a pivot. Thus their entire contribution uses only the product of those primes.

theorem grouped_incoming_row {K I : Type*} [Fintype K] [Fintype I]
    (P : K → ℕ) (Q : I → ℕ) {q : ℕ} (χ : DirichletCharacter ℂ q)
    (g : (K ⊕ I) → (K ⊕ I) → ℤ)
    (b : Option I → Option I → ℤ) (i : I)
    (hpivot : ∀ k, g (.inr i) (.inl k) = b (some i) none)
    (hrest : ∀ j, g (.inr i) (.inr j) = b (some i) (some j)) :
    (∏ j, χ ((Sum.elim P Q j : ℕ) : ZMod q) ^ g (.inr i) j) =
      retainedGraphRow χ b i ((∏ k, P k : ℕ) : ZMod q)
        (fun j => (Q j : ZMod q)) := by
…

Mentions: OAI.Ostmann.retainedGraphRow

def OAI.Ostmann.retainedGroupedPhase line 39

Source documentation

The phase left after the outgoing pivot rows have been removed.

noncomputable def retainedGroupedPhase {I : Type*} [Fintype I] (Q : I → ℕ)
    [∀ i, NeZero (Q i)] (χ : ∀ i, DirichletCharacter ℂ (Q i))
    (t : ∀ i, ZMod (Q i)) (ν : I → ℂ)
    (b : Option I → Option I → ℤ) (M : ℕ) (v : ℤ) : ℂ :=
…

theorem OAI.Ostmann.directedPrimePhase_remove_grouped_pivot line 48

Source documentation

Literal partition of the full directed phase. No cancellation or estimate is assumed: every incoming pivot edge remains in the retained phase.

theorem directedPrimePhase_remove_grouped_pivot {K I : Type*} [Fintype K] [Fintype I]
    (p : K ⊕ I → ℕ) [∀ j, NeZero (p j)]
    (χ : ∀ j, DirichletCharacter ℂ (p j))
    (t : ∀ j, ZMod (p j)) (ν : (K ⊕ I) → ℂ)
    (g : (K ⊕ I) → (K ⊕ I) → ℤ) (b : Option I → Option I → ℤ)
    (ε : K → ℤ) (v : ℤ)
    (hself : ∀ k, g (.inl k) (.inl k) = 0)
    (hrow : ∀ k j, j ≠ .inl k → g (.inl k) j = ε k)
    (hpivot : ∀ i k, g (.inr i) (.inl k) = b (some i) none)
    (hrest : ∀ i j, g (.inr i) (.inr j) = b (some i) (some j)) :
    directedPrimePhase p χ t ν g v =
      (∏ k, ZMod.stdAddChar (t (.inl k) *
…

Mentions: OAI.Ostmann.directedPrimePhase