VelocityClosedGraph.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Closed graph of actual component velocities

Exponential recovery and the closed probability-stabilizer graph imply that the graph of the actual velocity subspace is closed. In particular, compact restrictions can be projected without making an arbitrary choice of tangent curves or frames.

theorem OAI.DukePrimeDegree.isClosed_probability_velocity_graph line 24

theorem OAI.DukePrimeDegree.isClosed_probability_velocity_inter_compact line 44

Source documentation

Restricting the velocity variable to a fixed compact set gives a closed event in the space of probabilities.

theorem isClosed_probability_velocity_inter_compact (n : ℕ) [Nonempty (Fin n)]
    (K : Set (Matrix (Fin n) (Fin n) ℝ)) (hK : IsCompact K) :
    IsClosed {μ : ProbabilityMeasure (X n) | ∃ V ∈ K,
      V ∈ matrixVelocitySpace (invariantRightSubgroup (μ : Measure (X n)))} := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace

def OAI.DukePrimeDegree.probabilityVelocityDistance line 64
Source documentation
Distance to the actual velocity subspace, measured using the fixed matrix norm.
```
def probabilityVelocityDistance (n : ℕ)
    (V : Matrix (Fin n) (Fin n) ℝ) (μ : ProbabilityMeasure (X n)) : ℝ :=
…
```
theorem OAI.DukePrimeDegree.lowerSemicontinuous_probabilityVelocityDistance line 71
Source documentation
A closed graph and finite-dimensional compactness make the distance to the genuine velocity subspace lower semicontinuous. This is a useful measurability route that does not select tangent curves.
```
theorem lowerSemicontinuous_probabilityVelocityDistance (n : ℕ)
    [Nonempty (Fin n)] (V : Matrix (Fin n) (Fin n) ℝ) :
    LowerSemicontinuous (probabilityVelocityDistance n V) := by
…
```
Mentions: OAI.DukePrimeDegree.probabilityVelocityDistance