OAI/Analysis/FiniteFactor/CrossedProduct/IndicatorProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceIndicatorProjection line 12
2. theorem OAI.FiniteFactor.sourceIndicatorProjection_mem line 17
3. theorem OAI.FiniteFactor.sourceIndicatorProjection_projection line 21
4. theorem OAI.FiniteFactor.sourceIndicatorProjection_trace line 44

   Source documentation

   The projection's trace is the measure of its original base event.

   theorem sourceIndicatorProjection_trace (θ : SourceCoordinate → ℝ)
       (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A) :
       sourceVacuumFunctional (sourceIndicatorProjection θ A hA) =
         ((sourceBaseMeasure A).toReal : ℂ) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceVacuumFunctional, OAI.FiniteFactor.sourceIndicatorProjection, OAI.FiniteFactor.sourceBaseMeasure

5. theorem OAI.FiniteFactor.sourceIndicatorProjection_partition_sum line 60

   Source documentation

   A genuine finite partition of the identity inside the original algebra.

   theorem sourceIndicatorProjection_partition_sum (θ : SourceCoordinate → ℝ) (n : ℕ) (hn : 0 < n) :
       (∑ j : Fin n, sourceIndicatorProjection θ (sourceSmallPartitionSet n j)
         (sourceSmallPartitionSet_measurable n j)) = 1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceIndicatorProjection, OAI.FiniteFactor.sourceSmallPartitionSet, OAI.FiniteFactor.sourceSmallPartitionSet_measurable