SingleBlockShell.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A fixed compact set of transverse shearing limits

Normalizing the selected block makes the within-block part of every limiting conjugate equal to the identity. A fixed positive displacement therefore gives a compact set disjoint from the block group. Local containment of the actual stabilizer in that group supplies a sufficiently small displacement, before the generic points or the limiting shear are chosen.

lemma OAI.DukePrimeDegree.entry_sub_le_slMatrixDifference line 24
lemma OAI.DukePrimeDegree.continuous_withinBlockPart line 32
def OAI.DukePrimeDegree.transverseMatrixShell line 44
lemma OAI.DukePrimeDegree.transverseMatrixShell_isClosed line 47
lemma OAI.DukePrimeDegree.transverseMatrixShell_isCompact line 54
lemma OAI.DukePrimeDegree.transverseMatrixShell_not_mem_block line 76
theorem OAI.DukePrimeDegree.exists_small_transverse_shell line 99
Source documentation
Local block preservation gives a displacement scale whose entire transverse shell is disjoint from the actual subgroup.
```
theorem exists_small_transverse_shell {n : ℕ}
    (L : Subgroup (G n)) (r : Setoid (Fin n))
    (hlocal : {g : L | g.val ∈ blockMatrixGroup r} ∈ 𝓝 (1 : L)) :
    ∃ a : ℝ, 0 < a ∧ ∀ g ∈ transverseMatrixShell r a, g ∉ L := by
…
```
Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.transverseMatrixShell
theorem OAI.DukePrimeDegree.singleBlock_conjugation_limit_withinPart line 118

theorem OAI.DukePrimeDegree.exists_finite_small_transverse_separators line 145

Source documentation

The finitely many tests are fixed using the local stabilizer before the normalized pairs and their subsequences are selected.

theorem exists_finite_small_transverse_separators {n : ℕ}
    (μ : Measure (X n)) [IsFiniteMeasure μ]
    (r : Setoid (Fin n))
    (hlocal : {g : invariantRightSubgroup μ | g.val ∈ blockMatrixGroup r} ∈
      𝓝 (1 : invariantRightSubgroup μ)) :
    ∃ a : ℝ, 0 < a ∧
      ∃ (F : Finset (CompactlySupportedContinuousMap (X n) ℝ)) (ε : ℝ),
        0 < ε ∧ ∀ g ∈ transverseMatrixShell r a,
          ∃ f ∈ F, ε < |invarianceDefect μ f g| := by
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.transverseMatrixShell, OAI.DukePrimeDegree.invarianceDefect