OAI/Analysis/FiniteFactor/Fiber/StrongContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.fiberField_continuousOn line 13

   Source documentation

   A uniformly bounded field is strongly continuous wherever all its basis columns are continuous. No norm-continuity of the field is required.

   theorem fiberField_continuousOn {X : Type*} [TopologicalSpace X]
       (A : X → SourceFiberHilbert →L[ℂ] SourceFiberHilbert) (Q : Set X)
       (C : ℝ) (hC : ∀ x ∈ Q, ‖A x‖ ≤ C)
       (hb : ∀ k : ℤ, ContinuousOn (fun x => A x (lp.single 2 k (1 : ℂ))) Q)
       (v : SourceFiberHilbert) : ContinuousOn (fun x => A x v) Q := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert

2. theorem OAI.FiniteFactor.fiberField_continuousOn_apply line 47

   Source documentation

   Evaluation on a varying continuous vector preserves strong continuity under a uniform operator bound.

   theorem fiberField_continuousOn_apply {X : Type*} [TopologicalSpace X]
       (A : X → SourceFiberHilbert →L[ℂ] SourceFiberHilbert) (Q : Set X)
       (C : ℝ) (hC : ∀ x ∈ Q, ‖A x‖ ≤ C)
       (hA : ∀ v, ContinuousOn (fun x => A x v) Q)
       (v : X → SourceFiberHilbert) (hv : ContinuousOn v Q) :
       ContinuousOn (fun x => A x (v x)) Q := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert