BlockEliminationSchedule.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

A full within-block elimination schedule

Upper entries are cleared in increasing row order, and lower entries in decreasing row order. Transitivity of the block relation ensures that each affected earlier entry has an earlier zero source entry.

def OAI.DukePrimeDegree.blockUpperEntries line 21
def OAI.DukePrimeDegree.blockLowerEntries line 24
def OAI.DukePrimeDegree.blockOffDiagonalEntries line 27
lemma OAI.DukePrimeDegree.mem_blockUpperEntries line 30
lemma OAI.DukePrimeDegree.mem_blockLowerEntries line 34
lemma OAI.DukePrimeDegree.mem_blockOffDiagonalEntries line 38
def OAI.DukePrimeDegree.UpperInitial line 52
theorem OAI.DukePrimeDegree.exists_upper_schedule line 56
def OAI.DukePrimeDegree.LowerInitial line 108
theorem OAI.DukePrimeDegree.exists_lower_schedule line 112
theorem OAI.DukePrimeDegree.exists_block_elimination_schedule line 183
Source documentation
Every off-diagonal entry inside a block can be eliminated using only roots from that block, with every earlier zero retained.
```
theorem exists_block_elimination_schedule {n : ℕ} (r : Setoid (Fin n)) :
    ∃ c : BlockEliminationChain r ∅, c.finalEntries = blockOffDiagonalEntries r := by
…
```
Mentions: OAI.DukePrimeDegree.BlockEliminationChain, OAI.DukePrimeDegree.blockOffDiagonalEntries

theorem OAI.DukePrimeDegree.exists_block_transverse_sequence line 197

Source documentation

A near-identity sequence has an actual within-block root correction which kills all its within-block off-diagonal entries.

theorem exists_block_transverse_sequence {n : ℕ} (r : Setoid (Fin n))
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1)) :
    ∃ 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, ∀ i j, i ≠ j → r i j → (s k).val i j = 0 := by
…

Mentions: OAI.DukePrimeDegree.blockRootGroup

theorem OAI.DukePrimeDegree.exists_subgroup_transverse_sequence line 213

Source documentation

The correction lies in the original subgroup and preserves being outside it; membership of the full block group is not assumed.

theorem exists_subgroup_transverse_sequence {n : ℕ}
    (r : Setoid (Fin n)) (L : Subgroup (G n))
    (hroot : ∀ (i j : Fin n) (hij : i ≠ j), r i j → ∀ t : ℝ,
      Matrix.SpecialLinearGroup.transvection hij t ∈ L)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1)) (hout : ∀ k, g k ∉ L) :
    ∃ s b : ℕ → G n,
      Tendsto s atTop (𝓝 1) ∧ Tendsto b atTop (𝓝 1) ∧
      (∀ k, s k = g k * b k) ∧ (∀ k, b k ∈ L) ∧ (∀ k, s k ∉ L) ∧
      ∀ᶠ k in atTop, ∀ i j, i ≠ j → r i j → (s k).val i j = 0 := by
…