PairedBlockOrbit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One root pair excludes every proper block partition

The roots required here are just one opposite pair inside the actual finite orbit group. The partition may combine all singleton coordinates into one block; no root invariance is required among those coordinates. Thus this endpoint matches the open block subgroup provided by local projection fixation, without adding a diagonal-normalization hypothesis.

theorem OAI.DukePrimeDegree.partition_universal_of_generic_finite_opposite_root_orbit line 23

theorem OAI.DukePrimeDegree.partition_universal_of_generic_opposite_root_orbit_measure line 57

Source documentation

Transfer to a finite invariant measure on the actual lattice space, with its closed orbit group explicitly given.

theorem partition_universal_of_generic_opposite_root_orbit_measure {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ k, v k ≠ 0)
    (L : Subgroup (G n)) (hL : IsClosed (L : Set (G n)))
    (μ : Measure (X n)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g L))
    (hinv : ∀ h : L, μ.map (fun x => rightAction x h.val) = μ)
    (i j : Fin n) (hij : i ≠ j)
    (hroot_ij : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (hroot_ji : Matrix.SpecialLinearGroup.transvection hij.symm (1 : ℝ) ∈ L)
    (r : Setoid (Fin n)) (hblock : L ≤ blockMatrixGroup r) : ∀ a b, r a b := by
…

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

theorem OAI.DukePrimeDegree.partition_universal_of_open_opposite_root_orbit line 81

Source documentation

Only an open block-preserving subgroup is needed. The one opposite root pair lies in it because its two indices belong to the same block.

theorem partition_universal_of_open_opposite_root_orbit {n : ℕ}
    (hn : n.Prime) (g : G n) (L : Subgroup (G n))
    (hL : IsClosed (L : Set (G n)))
    (r : Setoid (Fin n))
    (hopen : IsOpen (((blockMatrixGroup r).comap L.subtype : Subgroup L) : Set L))
    (i j : Fin n) (hij : i ≠ j) (hr : r i j)
    (hroot_ij : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (hroot_ji : Matrix.SpecialLinearGroup.transvection hij.symm (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 → ∀ k, v k ≠ 0) :
…

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