OAI/NumberTheory/DukePrimeDegree/Dynamics/BlockTransverseElimination.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing block directions by actual invariant roots

This is a sequence-level Gaussian elimination. No Lie-subgroup classification or membership of the entire block group is assumed. Every correction is a product of the specified within-block roots. Pivots are eventually nonzero because the matrices tend to the identity.

  1. def OAI.DukePrimeDegree.BlockZeroPattern line 22
  2. lemma OAI.DukePrimeDegree.blockZeroPattern_translate line 25
  3. inductive OAI.DukePrimeDegree.BlockEliminationChain line 39

    Source documentation

    An elimination schedule records only zeros that must be preserved; nonzero pivots are supplied locally by convergence to the identity.

    inductive BlockEliminationChain {n : ℕ} (r : Setoid (Fin n)) :
    Finset (Fin n × Fin n) → Type
  | done {P} : BlockEliminationChain r P
  | step {P} (a b : Fin n) (hab : a ≠ b) (hr : r a b)
      (hP : ∀ j, (j, b) ∈ P → (j, a) ∈ P)
      (tail : BlockEliminationChain r (insert (a, b) P)) : BlockEliminationChain r P

namespace BlockEliminationChain

variable {n : ℕ} {r : Setoid (Fin n)} {P : Finset (Fin n × Fin n)}
  4. def OAI.DukePrimeDegree.BlockEliminationChain.finalEntries line 50
  5. def OAI.DukePrimeDegree.BlockEliminationChain.append line 55
  6. lemma OAI.DukePrimeDegree.BlockEliminationChain.finalEntries_append line 61
  7. theorem OAI.DukePrimeDegree.BlockEliminationChain.normalize_sequence line 70

    Source documentation

    The correction converges to one, belongs to the actual root-generated subgroup at every index, and eventually clears the entire schedule.

    theorem normalize_sequence (c : BlockEliminationChain r P)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1))
    (hzero : ∀ᶠ k in atTop, BlockZeroPattern P (g k)) :
    ∃ s b : ℕ → G n,
      Tendsto s atTop (𝓝 1) ∧ Tendsto b atTop (𝓝 1) ∧
      (∀ k, s k = g k * b k) ∧
      (∀ k, b k ∈ blockRootGroup r) ∧
      ∀ᶠ k in atTop, BlockZeroPattern c.finalEntries (s k) := by
…

    Mentions: OAI.DukePrimeDegree.BlockEliminationChain, OAI.DukePrimeDegree.BlockZeroPattern, OAI.DukePrimeDegree.blockRootGroup