OAI/Analysis/FiniteFactor/CrossedProduct/Reflection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceReflectionIndex line 11

   Source documentation

   The reflection for the source regular representation.

   def sourceReflectionIndex (θ : SourceCoordinate → ℝ)
       (z : (SourceCoordinate → ℝ) × ℤ) : (SourceCoordinate → ℝ) × ℤ :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

2. theorem OAI.FiniteFactor.sourceReflectionIndex_preserving line 15
3. def OAI.FiniteFactor.sourceReflectionLinear line 32
4. def OAI.FiniteFactor.sourceConjugation line 37

   Source documentation

   Explicit conjugate-linear isometry; no modular or tracial property assumed.

   def sourceConjugation (θ : SourceCoordinate → ℝ) (f : SourceHilbert SourceCoordinate) :
       SourceHilbert SourceCoordinate := star (sourceReflectionLinear θ f)

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceReflectionLinear

5. theorem OAI.FiniteFactor.sourceConjugation_apply_ae line 40
6. theorem OAI.FiniteFactor.sourceConjugation_involutive line 51
7. theorem OAI.FiniteFactor.sourceL2_star_inner line 65
8. theorem OAI.FiniteFactor.sourceConjugation_inner line 75
9. theorem OAI.FiniteFactor.sourceConjugation_inner_symm line 80