OAI/Analysis/FiniteFactor/CrossedProduct/LusinCompact.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.exists_source_lusin_compact line 14

   Source documentation

   All cocycles and all vector columns of the actual operator field are continuous on one compact subset of any prescribed Borel conull set.

   theorem exists_source_lusin_compact (θ : SourceCoordinate → ℝ)
       (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate)
       {s : Set SourceTorus} (hs : MeasurableSet s) (hfull : ∀ᵐ z ∂sourceTorusHaar, z ∈ s)
       {ε : ℝ≥0∞} (hε : ε ≠ 0) :
       ∃ Q, Q ⊆ s ∧ IsCompact Q ∧ sourceTorusHaar Qᶜ < ε ∧
         (∀ k : ℤ, ContinuousOn
           (fun z => sourceCocycle θ sourceLogWeight k (sourceTorusRepresentative z)) Q) ∧
         (∀ k : ℤ, ContinuousOn
           (fun z => sourceTorusOperatorField H z (lp.single 2 k (1 : ℂ))) Q) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceTorusRepresentative, OAI.FiniteFactor.sourceTorusOperatorField