MeasurableStrongTests.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Measurability of countable strong approximation conditions

Only vector evaluation is required to be measurable. Countable tests then give a measurable implementer condition without placing the norm topology on the operator algebra.

def OAI.KadisonKastler.PrefixStrongTests line 23
theorem OAI.KadisonKastler.prefixStrongTests_iff line 28
theorem OAI.KadisonKastler.measurableSet_prefixStrongTests line 42
Source documentation
Every condition is a countable combination of measurable vector-norm inequalities. The operator maps need not be norm measurable.
```
theorem measurableSet_prefixStrongTests (ξ : ℕ → H) (T : X → H →L[ℂ] H)
    (S : X → ℕ → H →L[ℂ] H)
    (h : ∀ q l, Measurable (fun p => (T p - S p q) (ξ l))) :
    MeasurableSet {p | PrefixStrongTests ξ T S p} := by
…
```
Mentions: OAI.KadisonKastler.PrefixStrongTests
theorem OAI.KadisonKastler.measurableSet_countableStrongTests_range line 60

theorem OAI.KadisonKastler.measurableSet_operator_norm_le line 69

Source documentation

An operator norm bound is a countable measurable condition when evaluations on a dense vector family are measurable.

theorem measurableSet_operator_norm_le (ξ : ℕ → H) (hξ : DenseRange ξ)
    (T : X → H →L[ℂ] H) {a : ℝ} (ha : 0 ≤ a)
    (hT : ∀ n, Measurable (fun p => T p (ξ n))) :
    MeasurableSet {p | ‖T p‖ ≤ a} := by
…