OAI/NumberTheory/Ostmann/Construction/GroupedResidueRow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The entire outgoing pivot phase factors through the composite residue key

  1. def OAI.Ostmann.groupedResidueRow line 12
  2. theorem OAI.Ostmann.groupedResidueRow_norm_le_one line 19
  3. theorem OAI.Ostmann.grouped_outgoing_local line 28

    Source documentation

    A local outgoing factor is exactly the bounded residue row. The hypotheses are the literal cofactor and unit conditions of the supported prime tuple.

    theorem grouped_outgoing_local {p : ℕ} [Fact p.Prime]
    (χ : DirichletCharacter ℂ p) (κ : ℂ) (t : ZMod p)
    (D H Y M : ℕ) (hM : 0 < M) (v ε : ℤ)
    (hpM : p ∣ M) (hHM : H.Coprime M)
    (hD : (D : ZMod p) ≠ 0) (hY : (Y : ZMod p) ≠ 0)
    (hv : (v : ZMod p) ≠ 0) :
    ZMod.stdAddChar (t * (((D * H * Y : ℕ) : ZMod p)⁻¹ * (v : ZMod p))) *
      (κ * χ (v : ZMod p) ^ (-ε)) * χ ((D * H * Y : ℕ) : ZMod p) ^ ε =
    pivotLocalRow χ κ t (D : ZMod p) (Y : ZMod p)
      ((positiveIntegerPivotKey M hM H v).val : ZMod p) ε := by
…

    Mentions: OAI.Ostmann.pivotLocalRow, OAI.Ostmann.positiveIntegerPivotKey