SingleBlockLocalStabilizer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From the velocity projection to actual local block preservation

Fixing the selected coordinate projection is exactly preservation of that block and its complement. This translates the proved velocity argument into the local subgroup statement used to choose a transverse shearing shell.

theorem OAI.DukePrimeDegree.singleBlockProjection_fixed_iff line 22
theorem OAI.DukePrimeDegree.local_singleBlock_of_fixed_projection line 46

theorem OAI.DukePrimeDegree.singleBlock_velocity_local_stabilizer line 56

Source documentation

The actual velocity-support conclusion gives precisely the local block containment needed by exists_small_transverse_shell.

theorem singleBlock_velocity_local_stabilizer {n : ℕ}
    (L : Subgroup (G n)) (S : Set (Fin n))
    (k l : Fin n) (hkl : k ≠ l) (hk : k ∈ S) (hl : l ∈ S)
    (hroot : ∀ i ∈ S, ∀ j ∈ S, ∀ (hij : i ≠ j) (t : ℝ),
      Matrix.SpecialLinearGroup.transvection hij t ∈ L)
    (hsupport : ∀ V ∈ matrixVelocitySpace L, ∀ i j,
      ¬(i ∈ S ↔ j ∈ S) → V i j = 0) :
    {g : L | g.val ∈ blockMatrixGroup (blockComplementSetoid S)} ∈ 𝓝 (1 : L) :=
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace, OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.blockComplementSetoid