OAI/Analysis/FiniteFactor/CrossedProduct/FiberIndicators.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceBaseIndicator line 12

   Source documentation

   Bounded measurable indicator on the base.

   def sourceBaseIndicator (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A) :
       SourceBaseFunction where
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBaseFunction

2. theorem OAI.FiniteFactor.sourceFiberMeasure_ne_top line 20
3. def OAI.FiniteFactor.sourceFiberIndicator line 25
4. theorem OAI.FiniteFactor.sourceFiberIndicator_coe line 29
5. theorem OAI.FiniteFactor.sourceVacuum_coe line 34
6. theorem OAI.FiniteFactor.sourceFiberIndicator_eq_orbit line 40

   Source documentation

   Every bounded base indicator on an arbitrary fiber is in the vacuum's commutant orbit. No cyclicity or separating property is assumed.

   theorem sourceFiberIndicator_eq_orbit (θ : SourceCoordinate → ℝ)
       (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A) (n : ℤ) :
       sourceFiberIndicator A hA n = sourceScalar (sourceBaseIndicator A hA)
         (sourceCommutantRotation θ n sourceVacuum) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceFiberIndicator, OAI.FiniteFactor.sourceScalar, OAI.FiniteFactor.sourceBaseIndicator, OAI.FiniteFactor.sourceCommutantRotation, OAI.FiniteFactor.sourceVacuum