MultiplicationAdjoint.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceBaseStar line 12
Source documentation
Conjugate of a bounded source base function, with the same bound.
```
def sourceBaseStar (g : SourceBaseFunction) : SourceBaseFunction where
…
```
Mentions: OAI.FiniteFactor.SourceBaseFunction
theorem OAI.FiniteFactor.sourcePi_star line 20
Source documentation
The multiplication representation has the actual Hilbert adjoint.
```
theorem sourcePi_star (θ : SourceCoordinate → ℝ) (g : SourceBaseFunction) :
    star (sourcePi θ g) = sourcePi θ (sourceBaseStar g) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.sourcePi, OAI.FiniteFactor.sourceBaseStar
theorem OAI.FiniteFactor.sourcePi_commute line 35
Source documentation
Any two such multiplication operators commute, even for different angles.
```
theorem sourcePi_commute (θ φ : SourceCoordinate → ℝ) (g h : SourceBaseFunction) :
    sourcePi θ g * sourcePi φ h = sourcePi φ h * sourcePi θ g := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.sourcePi