OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockClosure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact corrections from the closure of one root block

Haar patches are taken in the closed root-generated subgroup. This closure still preserves the same finite measure. Continuity preserves the exact normalization of the within-block matrix part, so no abstract Lie-subgroup or homogeneous-orbit statement is needed for these patches.

  1. lemma OAI.DukePrimeDegree.singleBlock_closure_le_stabilizer line 22
  2. lemma OAI.DukePrimeDegree.singleBlock_closure_le_blockComplement line 28
  3. lemma OAI.DukePrimeDegree.withinBlockPart_singleBlock_closure_commutes line 34
  4. theorem OAI.DukePrimeDegree.withinBlockPart_singleBlock_closure_conjugation line 47