OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockLocalNeutralMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The measure in an open neutral-subgroup chart

Only an open subgroup of the neutral group is used. Thus the chart applies to the actual subgroup proved to preserve the measure, without imposing invariance under disconnected components of the neutral centralizer.

  1. instance OAI.DukePrimeDegree.twoBlockSL_measurableSpace line 20
  2. instance OAI.DukePrimeDegree.twoBlockSL_borelSpace line 23
  3. instance OAI.DukePrimeDegree.twoBlockSL_secondCountable line 25
  4. abbrev OAI.DukePrimeDegree.TwoBlockTransverse line 30
  5. instance OAI.DukePrimeDegree.twoBlockTransverse_borelSpace line 33
  6. instance OAI.DukePrimeDegree.twoBlockTransverse_secondCountable line 36
  7. def OAI.DukePrimeDegree.twoBlockLocalNeutralParam line 40
  8. theorem OAI.DukePrimeDegree.twoBlockLocalNeutralParam_isOpenEmbedding line 44
  9. theorem OAI.DukePrimeDegree.twoBlockLocalNeutralParam_right line 55
  10. def OAI.DukePrimeDegree.twoBlockLocalNeutralMeasure line 62
  11. theorem OAI.DukePrimeDegree.twoBlockLocalNeutralMeasure_finiteOnCompacts line 67
  12. theorem OAI.DukePrimeDegree.twoBlockLocalNeutralMeasure_right_invariant line 76