TransverseStabilizerLimit.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A transverse diagonal limit lies outside the stabilizer

The previously proved commutator identities give a global statement: an element of L with nonzero diagonal preserves the maximal root blocks. Consequently a nonidentity diagonal-conjugation limit with zero within-block off-diagonal entries cannot belong to L. No additional "limit outside L" assumption or connectedness assumption is used.

lemma OAI.DukePrimeDegree.mem_blockMatrixGroup_of_cross_zero line 24
lemma OAI.DukePrimeDegree.cross_zero_of_mem_blockMatrixGroup line 36
theorem OAI.DukePrimeDegree.mem_blocks_of_projection_products_and_nonzero_diagonal line 47
Source documentation
No smallness condition is required: using the nonzero diagonal entry in each conjugated coordinate projection makes the inverse block diagonal, hence the matrix itself block diagonal.
```
theorem mem_blocks_of_projection_products_and_nonzero_diagonal {n : ℕ}
    (r : Setoid (Fin n)) (g : G n)
    (hproducts : ∀ i j, ¬ r i j → ∀ k, g.val i k * g⁻¹.val k j = 0)
    (hdiag : ∀ i, g.val i i ≠ 0) : g ∈ blockMatrixGroup r := by
…
```
Mentions: OAI.DukePrimeDegree.blockMatrixGroup
theorem OAI.DukePrimeDegree.transverse_member_eq_one line 57

theorem OAI.DukePrimeDegree.transverse_not_mem_of_maximal_roots line 77

Source documentation

This endpoint uses the actual maximal-root property, already available for the invariant-root equivalence relation.

theorem transverse_not_mem_of_maximal_roots {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 : G n) (hne : g ≠ 1) (hdiag : ∀ i, g.val i i = 1)
    (hwithin : ∀ i j, i ≠ j → r i j → g.val i j = 0) : g ∉ L := by
…

theorem OAI.DukePrimeDegree.diagonal_transverse_limit_entries line 94

Source documentation

Diagonal rescaling preserves every cleared within-block entry and leaves the diagonal unchanged, including for diverging rescaling times.

theorem diagonal_transverse_limit_entries {n : ℕ}
    (r : Setoid (Fin n)) (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1))
    (hzero : ∀ᶠ k in atTop, ∀ i j, i ≠ j → r i j → (g k).val i j = 0)
    (ell : Fin n → ℝ) (hsum : ∑ i, ell i = 0) (t : ℕ → ℝ)
    (h : G n)
    (hlim : Tendsto (fun k => diagonalOneParameter ell hsum (t k) * g k *
      diagonalOneParameter ell hsum (-t k)) atTop (𝓝 h)) :
    (∀ i, h.val i i = 1) ∧ (∀ i j, i ≠ j → r i j → h.val i j = 0) := by
…

theorem OAI.DukePrimeDegree.diagonal_transverse_limit_not_mem line 120

theorem OAI.DukePrimeDegree.actual_invariant_subgroup_transverse_not_mem line 139

Source documentation

Specialization to the actual finite-measure stabilizer. All subgroup closedness, normalization, and maximal-root hypotheses are proved here from A-invariance and the actual invariant-root relation.

theorem actual_invariant_subgroup_transverse_not_mem
    (d : ℕ) (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (r : Setoid (Fin (d + 1)))
    (hr : ∀ i j, r i j ↔ rootInvarianceRelation μ i j)
    (g : G (d + 1)) (hne : g ≠ 1) (hdiag : ∀ i, g.val i i = 1)
    (hwithin : ∀ i j, i ≠ j → r i j → g.val i j = 0) :
    g ∉ invariantRightSubgroup μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow