ConjugationVacuum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceConjugation_fiberIndicator line 11
Source documentation
Reflection of each total vacuum test equals its commutant adjoint on the vacuum.
```
theorem sourceConjugation_fiberIndicator (θ : SourceCoordinate → ℝ)
    (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A) (n : ℤ) :
    sourceConjugation θ (sourceFiberIndicator A hA n) =
      star (sourceScalar (sourceBaseIndicator A hA) * sourceCommutantRotation θ n) sourceVacuum := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceConjugation, OAI.FiniteFactor.sourceFiberIndicator, OAI.FiniteFactor.sourceScalar, OAI.FiniteFactor.sourceBaseIndicator, OAI.FiniteFactor.sourceCommutantRotation, OAI.FiniteFactor.sourceVacuum
theorem OAI.FiniteFactor.sourceConjugation_algebra_vacuum line 44
Source documentation
The actual reflection sends H e_0 to H* e_0 for every source-algebra element.
```
theorem sourceConjugation_algebra_vacuum (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) :
    sourceConjugation θ (H sourceVacuum) = star H sourceVacuum := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceConjugation, OAI.FiniteFactor.sourceVacuum