OpenSubgroupOrbit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Selecting a positive-mass orbit of an open subgroup

An open subgroup has countable index in the second-countable matrix groups used here. A finite invariant measure on a larger orbit therefore has a nonzero restriction to one smaller orbit. The generic full set is preserved by restriction, allowing the basepoint to be chosen there. No connectedness of the larger homogeneous group is needed.

lemma OAI.DukePrimeDegree.countable_quotient_of_open_subgroup line 23
lemma OAI.DukePrimeDegree.larger_orbit_covered_by_subgroup_orbits line 30
lemma OAI.DukePrimeDegree.latticeOrbitPoint_range_mul line 47
lemma OAI.DukePrimeDegree.restrict_orbit_invariant line 66

theorem OAI.DukePrimeDegree.exists_nonzero_subgroup_orbit_restriction line 78

Source documentation

An actual larger orbit decomposes into countably many orbits of an open subgroup, one of which has positive measure.

theorem exists_nonzero_subgroup_orbit_restriction {n : ℕ}
    (g : G n) (L H : Subgroup (G n)) (hHL : H ≤ L)
    (hopen : IsOpen ((H.comap L.subtype : Subgroup L) : Set L))
    (μ : Measure (X n)) (hμ : μ ≠ 0)
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g L)) :
    ∃ g' : G n, μ.restrict (range (latticeOrbitPoint g' H)) ≠ 0 := by
…

Mentions: OAI.DukePrimeDegree.latticeOrbitPoint

theorem OAI.DukePrimeDegree.root_partition_universal_of_open_blockSubgroup_orbit line 103

Source documentation

The prime-degree obstruction needs only an open block-preserving subgroup of the actual finite-volume orbit group.

theorem root_partition_universal_of_open_blockSubgroup_orbit {n : ℕ}
    (hn : n.Prime) (g : G n) (L : Subgroup (G n))
    (hL : IsClosed (L : Set (G n)))
    (r : Setoid (Fin n)) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (hopen : IsOpen (((blockMatrixGroup r).comap L.subtype : Subgroup L) : Set L))
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (μ : Measure (X n)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g L))
    (hinv : ∀ h : L, μ.map (fun x => rightAction x h.val) = μ)
    (hgeneric : ∀ᵐ x ∂μ, ∀ v ∈ pointLattice x, v ≠ 0 → ∀ j, v j ≠ 0) :
    ∀ i j, r i j := by
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.latticeOrbitPoint