FreeProductMatrixContinuity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of the constructed finite matrix action follows from ordinary factor-algebra density and the isometry bound; it is not an extra free-product or Haar-averaging hypothesis.

def OAI.KadisonSimilarity.continuousOrbitSubmodule line 24
Source documentation
Vectors with continuous orbit form a linear subspace.
```
def continuousOrbitSubmodule : Submodule ℂ H where
…
```
theorem OAI.KadisonSimilarity.continuousOrbitSubmodule_isClosed line 32
Source documentation
A common contraction bound makes the continuous-orbit subspace closed.
```
theorem continuousOrbitSubmodule_isClosed (hU : ∀ g, ‖U g‖ ≤ 1) :
    IsClosed (continuousOrbitSubmodule U : Set H) := by
…
```
Mentions: OAI.KadisonSimilarity.continuousOrbitSubmodule
theorem OAI.KadisonSimilarity.TracialCornerGeometry.continuous_vector line 59
Source documentation
The tracial vector map is continuous because it is left multiplication on its fixed vacuum vector.
```
theorem continuous_vector : Continuous G.vector := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.continuous_matrixConjugateLetter line 74
Source documentation
Conjugation of a fixed factor element depends continuously on the matrix unitary, directly from finite-dimensional continuity and multiplication.
```
theorem continuous_matrixConjugateLetter (d : D) :
    Continuous (fun u : Matrix.unitaryGroup α ℂ => (matrixConjugateLetter D ι u d : P)) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter
theorem OAI.KadisonSimilarity.TracialCornerGeometry.continuous_chosenMatrixExtension line 85
Source documentation
Every element of the algebra generated by the two factors has a continuous orbit in the original operator norm.
```
theorem continuous_chosenMatrixExtension (a : factorAlgebra A D) :
    Continuous (fun u : Matrix.unitaryGroup α ℂ => G.chosenMatrixExtension A D ι hext u (a : P)) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionUnitaryRepresentation_stronglyContinuous line 123
Source documentation
The actual free-product matrix representation is strongly continuous; only the ordinary tracial generation and published factor extension are used.
```
theorem matrixExtensionUnitaryRepresentation_stronglyContinuous (x : H) :
    Continuous (fun u : Matrix.unitaryGroup α ℂ =>
      (G.matrixExtensionUnitaryRepresentation A D ι hgen hfaithful hext u : H →L[ℂ] H) x) := by
…
```