PairedOrbitSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Root-invariant finite measures supported on a block orbit

The orbit measure need not be invariant under its entire orbit group. Only the two opposite root maps preserve it. Polynomial recurrence is applied to every rational stabilizer-commutant observable simultaneously; a generic point then makes that rational commutant scalar. This reduces the dynamical target to finding positive mass on a block orbit, rather than assuming a finite homogeneous invariant measure on that orbit.

lemma OAI.DukePrimeDegree.conjugationOrbitMap_map_invariant_element line 24
lemma OAI.DukePrimeDegree.ae_conjugationOrbitMap_commute_root line 44
lemma OAI.DukePrimeDegree.latticeRational_commutes_pointStabilizer line 64

theorem OAI.DukePrimeDegree.realStabilizer_scalar_of_root_pair_measure line 78

Source documentation

Full orbit-group invariance is unnecessary: recurrence for the two root maps and genericity almost everywhere suffice to make the actual integral-stabilizer commutant scalar.

theorem realStabilizer_scalar_of_root_pair_measure {n : ℕ}
    (hn : n.Prime) (g : G n) (L : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g L)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (i j : Fin n) (hij : i ≠ j)
    (hroot : Matrix.SpecialLinearGroup.transvection hij (-1 : ℝ) ∈ L)
    (hopposite : Matrix.SpecialLinearGroup.transvection hij.symm (-1 : ℝ) ∈ L)
    (hinv : μ.map (fun x => latticeOrbitRightAction g L x
      ⟨Matrix.SpecialLinearGroup.transvection hij (-1 : ℝ), hroot⟩) = μ)
    (hopinv : μ.map (fun x => latticeOrbitRightAction g L x
      ⟨Matrix.SpecialLinearGroup.transvection hij.symm (-1 : ℝ), hopposite⟩) = μ)
    (hgeneric : ∀ᵐ x ∂μ, ∀ v ∈ pointLattice (latticeOrbitPoint g L x),
      v ≠ 0 → ∀ k, v k ≠ 0)
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.latticeOrbitPoint