NormalizerOrbitReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

From a normalizer orbit to one block orbit

The finite normalizer quotient gives a finite cover by block-group orbits. Each such orbit is Borel and diagonal invariant. Diagonal ergodicity thus places the whole measure on one of them. These are direct consequences of an actual normalizer-orbit support statement, not an assertion that every root-invariant measure already has that support.

lemma OAI.DukePrimeDegree.latticeOrbitPoint_range_preimage line 23
lemma OAI.DukePrimeDegree.scalarNormalizer_orbit_covered_by_blockOrbits line 38

theorem OAI.DukePrimeDegree.exists_block_orbit_of_scalarNormalizer_orbit line 62

Source documentation

Diagonal ergodicity selects one block orbit from an actual normalizer orbit. No invariance under disconnected normalizer components is needed.

theorem exists_block_orbit_of_scalarNormalizer_orbit {d : ℕ}
    (g : G (d + 1)) (r : Setoid (Fin (d + 1)))
    (μ : Measure (X (d + 1))) (hμ : μ ≠ 0)
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g (blockScalarNormalizer r))) :
    ∃ g' : G (d + 1), ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g' (blockMatrixGroup r)) := by
…

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

theorem OAI.DukePrimeDegree.block_partition_universal_of_invariant_normalizerOrbit line 101

Source documentation

The prime-degree obstruction also applies to a measure supported on one full block-normalizer orbit.

theorem block_partition_universal_of_invariant_normalizerOrbit {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)
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g (blockScalarNormalizer r)))
    (hinv : ∀ h : blockMatrixGroup r, μ.map (fun x => rightAction x h.val) = μ) :
    ∀ i j, r i j := by
…

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