BlockMatrixProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The within-block matrix projection

The projection onto the within-block entries commutes with multiplication by block-diagonal matrices on either side. Hence a scalar within-block part stays scalar under every within-block conjugation, including the unipotent shears used in the stopping-time argument.

def OAI.DukePrimeDegree.withinBlockPart line 21
lemma OAI.DukePrimeDegree.withinBlockPart_mul_left line 25
lemma OAI.DukePrimeDegree.withinBlockPart_mul_right line 47
lemma OAI.DukePrimeDegree.withinBlockPart_eq_scalar_iff line 69
theorem OAI.DukePrimeDegree.withinBlockPart_conjugate_scalar line 94
Source documentation
Conjugation by any block matrix preserves the scalar within-block part. The cross-block part cannot produce a hidden within-block limit.
```
theorem withinBlockPart_conjugate_scalar {n : ℕ} (r : Setoid (Fin n))
    (g u : G n) (hu : u ∈ blockMatrixGroup r) (c : ℝ)
    (hg : withinBlockPart r g.val = Matrix.diagonal (fun _ => c)) :
    withinBlockPart r (u * g * u⁻¹).val = Matrix.diagonal (fun _ => c) := by
…
```
Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.withinBlockPart

theorem OAI.DukePrimeDegree.block_conjugation_transverse_limit_entries line 111

Source documentation

The conjugating block matrices may diverge. The scalar block part still tends to identity, and no within-block off-diagonal entry appears.

theorem block_conjugation_transverse_limit_entries {n : ℕ}
    (r : Setoid (Fin n)) (g u : ℕ → G n) (c : ℕ → ℝ)
    (hg : Tendsto g atTop (𝓝 1))
    (hu : ∀ k, u k ∈ blockMatrixGroup r)
    (hpart : ∀ᶠ k in atTop,
      withinBlockPart r (g k).val = Matrix.diagonal (fun _ => c k))
    (h : G n)
    (hlim : Tendsto (fun k => u k * g k * (u k)⁻¹) atTop (𝓝 h)) :
    (∀ i, h.val i i = 1) ∧ (∀ i j, i ≠ j → r i j → h.val i j = 0) := by
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.withinBlockPart

theorem OAI.DukePrimeDegree.block_conjugation_transverse_limit_not_mem line 146

Source documentation

In particular the existing root-shearing compactness theorem can never return a nonidentity element already in L after this normalization.

theorem block_conjugation_transverse_limit_not_mem {n : ℕ}
    (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n)))
    (hnormal : ∀ (ell : Fin n → ℝ) (hsum : ∑ i, ell i = 0) (t : ℝ),
      ∀ g ∈ L, diagonalOneParameter ell hsum t * g * diagonalOneParameter ell hsum (-t) ∈ L)
    (r : Setoid (Fin n))
    (hmax : ∀ (i j : Fin n) (hij : i ≠ j) (c : ℝ), c ≠ 0 →
      Matrix.SpecialLinearGroup.transvection hij c ∈ L → r i j)
    (g u : ℕ → G n) (c : ℕ → ℝ) (hg : Tendsto g atTop (𝓝 1))
    (hu : ∀ k, u k ∈ blockMatrixGroup r)
    (hpart : ∀ᶠ k in atTop,
      withinBlockPart r (g k).val = Matrix.diagonal (fun _ => c k))
    (h : G n) (hne : h ≠ 1)
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.withinBlockPart