StabilizerClosedGraph.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Closed graph of the actual probability stabilizer

The probability measure and the group element may both vary. Uniform translation control of compact observables shows that invariance passes to the simultaneous limit. This is the topological input for constructing measurable data from the component stabilizers.

theorem OAI.DukePrimeDegree.isClosed_probability_smul_stabilizer line 22
theorem OAI.DukePrimeDegree.isClosed_probability_right_stabilizer line 42
Source documentation
The actual right stabilizer on the row-lattice quotient has closed graph in the weak probability topology times the real matrix group.
```
theorem isClosed_probability_right_stabilizer (n : ℕ) :
    IsClosed {p : ProbabilityMeasure (X n) × G n |
      p.2 ∈ invariantRightSubgroup (p.1 : Measure (X n))} := by
…
```
theorem OAI.DukePrimeDegree.isClosed_probability_matrix_stabilizer line 68
Source documentation
Passing from an SL element to its actual matrix preserves the closed stabilizer graph because the determinant-one inclusion is a closed embedding.
```
theorem isClosed_probability_matrix_stabilizer (n : ℕ) :
    IsClosed {p : ProbabilityMeasure (X n) × Matrix (Fin n) (Fin n) ℝ |
      ∃ g : G n, g ∈ invariantRightSubgroup (p.1 : Measure (X n)) ∧ g.val = p.2} := by
…
```