OAI/Analysis/FiniteFactor/Fiber/PairZeroSet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.fiberPairResidual line 12

   Source documentation

   The actual bounded operator whose vanishing is the pair identity.

   def fiberPairResidual {X : Type*}
       (P : X → SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
       (d : X × X → ℤ → ℂ) (hd : ∀ z k, ‖d z k‖ ≤ 1) (z : X × X) :
       SourceFiberHilbert →L[ℂ] SourceFiberHilbert :=
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert

2. theorem OAI.FiniteFactor.fiberPairResidual_eq_zero_iff line 18
3. theorem OAI.FiniteFactor.fiberPairResidual_continuousOn line 31
4. theorem OAI.FiniteFactor.fiberPairResidual_stronglyMeasurable line 50
5. theorem OAI.FiniteFactor.fiberPairZeroSet_measurable line 63
6. theorem OAI.FiniteFactor.fiberPairZeroSet_compact line 74