OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockInvariantChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The two-block chart for the actual invariant lattice measure

The neutral subgroup here is the preimage of the actual measure stabilizer. Its openness is deduced from within-block root invariance and diagonal invariance, and covering-lift invariance supplies the translation invariance in the parabolic coordinates.

  1. theorem OAI.DukePrimeDegree.isClosed_twoBlockNeutralGroup line 23
  2. theorem OAI.DukePrimeDegree.twoBlockNeutralGroup_locallyCompact line 30
  3. def OAI.DukePrimeDegree.twoBlockMeasureStabilizer line 38
  4. theorem OAI.DukePrimeDegree.isOpen_twoBlockMeasureStabilizer line 43
  5. def OAI.DukePrimeDegree.twoBlockLiftMeasure line 54
  6. theorem OAI.DukePrimeDegree.twoBlockLiftMeasure_right_invariant line 58
  7. def OAI.DukePrimeDegree.actualTwoBlockCoordinateMeasure line 86
  8. theorem OAI.DukePrimeDegree.actualTwoBlockCoordinateMeasure_right_invariant line 91
  9. theorem OAI.DukePrimeDegree.actualTwoBlockCoordinateMeasure_finiteOnCompacts line 106
  10. theorem OAI.DukePrimeDegree.actualTwoBlockCoordinateMeasure_product line 124

    Source documentation

    The neutral factor is right Haar on the actual open invariant subgroup. There is no assertion that it is left Haar or that its modular character vanishes.

    theorem actualTwoBlockCoordinateMeasure_product {n a b : ℕ}
    (e : Fin n ≃ Fin a ⊕ Fin b) (hn : n ≠ 0) (μ : Measure (X n)) [IsFiniteMeasure μ]
    (s : X n → G n) (hsm : Measurable s)
    (hs : ∀ x, Quotient.mk (QuotientGroup.rightRel (integralGroup n)) (s x) = x)
    (hroot : ∀ (i j : Fin n) (hij : i ≠ j), (twoBlockIndexSetoid e) i j → ∀ t : ℝ,
      μ.map (fun x => rightAction x (SpecialLinearGroup.transvection hij t)) = μ)
    (hdiag : ∀ (v : Fin n → ℝ) (hv : ∑ i, v i = 0) (t : ℝ),
      μ.map (fun x => rightAction x (diagonalOneParameter v hv t)) = μ)
    (η : Measure (twoBlockMeasureStabilizer e μ)) [η.inv.IsHaarMeasure]
    (K : Set (twoBlockMeasureStabilizer e μ)) (hK : IsCompact K) (hηK : η K = 1) :
    actualTwoBlockCoordinateMeasure e μ s =
      (firstCoordinateSlice (actualTwoBlockCoordinateMeasure e μ s) K).prod η := by
…

    Mentions: OAI.DukePrimeDegree.twoBlockIndexSetoid, OAI.DukePrimeDegree.twoBlockMeasureStabilizer, OAI.DukePrimeDegree.actualTwoBlockCoordinateMeasure, OAI.DukePrimeDegree.firstCoordinateSlice