OAI/Analysis/FiniteFactor/CrossedProduct/FiberTotal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceFiberIndicators_total line 12

   Source documentation

   Measurable base indicators on the integer fibers determine an L2 vector.

   theorem sourceFiberIndicators_total (f : SourceHilbert SourceCoordinate)
       (hf : ∀ (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A) (n : ℤ),
         inner ℂ (sourceFiberIndicator A hA n) f = 0) : f = 0 := by
   …

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