OAI/Analysis/FiniteFactor/CrossedProduct/CappedPair.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceCappedRatio line 11
2. theorem OAI.FiniteFactor.sourceCappedRatio_norm line 15
3. theorem OAI.FiniteFactor.sourceCappedRatio_measurable line 21
4. theorem OAI.FiniteFactor.sourceCappedRatio_continuousOn line 30
5. def OAI.FiniteFactor.sourceCappedPairZeroSet line 42

   Source documentation

   The capped equation uses the previously constructed field of the original operator, on the actual sampling torus.

   def sourceCappedPairZeroSet (θ : SourceCoordinate → ℝ)
       (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) :
       Set (SourceTorus × SourceTorus) :=
   …

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

6. theorem OAI.FiniteFactor.sourceCappedPairZeroSet_measurable line 48
7. theorem OAI.FiniteFactor.exists_source_capped_compact line 56

   Source documentation

   The compact zero sets needed for Portmanteau are constructed from the actual field and original cocycles, with arbitrarily small Haar loss.

   theorem exists_source_capped_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ᶜ < ε ∧
         IsCompact ((Q ×ˢ Q) ∩ sourceCappedPairZeroSet θ H) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceCappedPairZeroSet