OAI/Analysis/FiniteFactor/Fiber/Diagonal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.fiberDiagonal line 12

   Source documentation

   A bounded diagonal on the original l2(Z) fiber.

   def fiberDiagonal (d : ℤ → ℂ) (hd : ∀ k, ‖d k‖ ≤ 1) :
       SourceFiberHilbert →L[ℂ] SourceFiberHilbert :=
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert

2. theorem OAI.FiniteFactor.fiberDiagonal_apply line 29
3. theorem OAI.FiniteFactor.fiberDiagonal_norm line 32
4. theorem OAI.FiniteFactor.fiberDiagonal_single line 36
5. theorem OAI.FiniteFactor.fiberDiagonal_continuousOn line 47
6. theorem OAI.FiniteFactor.fiberDiagonal_stronglyMeasurable line 56
7. theorem OAI.FiniteFactor.fiberField_stronglyMeasurable_apply line 66

   Source documentation

   Applying a measurable field to a measurable vector uses finite coordinate approximations, without measurability in the operator norm topology.

   theorem fiberField_stronglyMeasurable_apply {X : Type*} [MeasurableSpace X]
       (A : X → SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
       (hA : ∀ v, StronglyMeasurable (fun x => A x v))
       (v : X → SourceFiberHilbert) (hv : StronglyMeasurable v) :
       StronglyMeasurable (fun x => A x (v x)) := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert