OrbitMeasureTransfer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Invariant measures on actual lattice orbits

The quotient by the actual point stabilizer injects into the lattice space. For a closed matrix subgroup this injection is a Borel embedding, even when the orbit is not closed. A finite invariant measure concentrated on that orbit therefore pulls back to a finite invariant measure on the quotient.

This discharges the measure-transfer part of the homogeneous-orbit argument; it does not assert the existence of a homogeneous orbit supporting a given measure.

lemma OAI.DukePrimeDegree.latticeOrbitPoint_injective line 26
lemma OAI.DukePrimeDegree.measurableEmbedding_of_continuous_injective_sigmaCompact line 41
lemma OAI.DukePrimeDegree.latticeOrbitPoint_measurableEmbedding line 75
lemma OAI.DukePrimeDegree.isClosed_blockMatrixGroup line 89

lemma OAI.DukePrimeDegree.latticeOrbitPoint_map_comap line 108

Source documentation

Pullback through the actual orbit injection recovers the ambient measure when that measure is concentrated on the orbit.

lemma latticeOrbitPoint_map_comap {n : ℕ} (g : G n) (H : Subgroup (G n))
    (hH : IsClosed (H : Set (G n))) (μ : Measure (X n))
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g H)) :
    (μ.comap (latticeOrbitPoint g H)).map (latticeOrbitPoint g H) = μ := by
…

Mentions: OAI.DukePrimeDegree.latticeOrbitPoint

lemma OAI.DukePrimeDegree.latticeOrbitPoint_comap_invariant line 115

theorem OAI.DukePrimeDegree.block_partition_universal_of_invariant_orbit_measure line 140

Source documentation

The prime-degree finite-orbit obstruction stated directly for a measure on the lattice space. No measure on a quotient is an additional hypothesis.

theorem block_partition_universal_of_invariant_orbit_measure {d : ℕ}
    (hn : (d + 1).Prime) (g : G (d + 1)) (r : Setoid (Fin (d + 1)))
    (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g (blockMatrixGroup r)))
    (hinv : ∀ h : blockMatrixGroup r, μ.map (fun x => rightAction x h.val) = μ) :
    ∀ i j, r i j := by
…

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