HilbertCoefficientMeasurable.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Measurability from countably many Hilbert coefficients

The coefficients against a countable dense family give a continuous injection into a countable product of copies of ℂ. Lusin–Souslin makes this map a measurable embedding. Thus measurability of the coefficients implies strong measurability, without assuming a Pettis theorem.

theorem OAI.KadisonKastler.aestronglyMeasurable_of_dense_inner line 28

Source documentation

Countably many dense coefficient tests determine a measurable vector field.

theorem aestronglyMeasurable_of_dense_inner [Countable ι]
    (v : ι → H) (hv : DenseRange v) (f : D → H)
    (hf : ∀ i, AEStronglyMeasurable (fun x => inner ℂ (v i) (f x)) μ) :
    AEStronglyMeasurable f μ := by
…

theorem OAI.KadisonKastler.aestronglyMeasurable_of_countable_dense_inner line 44

Source documentation

The same criterion stated using a countable dense subset.

theorem aestronglyMeasurable_of_countable_dense_inner
    (s : Set H) (hs : s.Countable) (hd : Dense s) (f : D → H)
    (hf : ∀ η ∈ s, AEStronglyMeasurable (fun x => inner ℂ η (f x)) μ) :
    AEStronglyMeasurable f μ := by
…

theorem OAI.KadisonKastler.aestronglyMeasurable_of_inner line 60
Source documentation
In a separable Hilbert space, measurable scalar coefficients imply strong measurability of the vector field.
```
theorem aestronglyMeasurable_of_inner (f : D → H)
    (hf : ∀ η : H, AEStronglyMeasurable (fun x => inner ℂ η (f x)) μ) :
    AEStronglyMeasurable f μ := by
…
```
theorem OAI.KadisonKastler.operator_adjoint_eval_aestronglyMeasurable line 68
Source documentation
Once a field has measurable evaluations, its adjoint does too. This uses the scalar adjoint identity and the preceding coefficient test.
```
theorem operator_adjoint_eval_aestronglyMeasurable
    (T : D → H →L[ℂ] H)
    (hT : ∀ ξ, AEStronglyMeasurable (fun x => T x ξ) μ) (η : H) :
    AEStronglyMeasurable (fun x => star (T x) η) μ := by
…
```

theorem OAI.KadisonKastler.operator_eval_aestronglyMeasurable_of_dense_coefficients line 79

Source documentation

Testing both variables only on a countable dense family suffices to make every evaluation of an operator field strongly measurable.

theorem operator_eval_aestronglyMeasurable_of_dense_coefficients [Countable ι]
    (v : ι → H) (hv : DenseRange v) (T : D → H →L[ℂ] H)
    (hT : ∀ i j, AEStronglyMeasurable (fun x => inner ℂ (v i) (T x (v j))) μ)
    (ξ : H) : AEStronglyMeasurable (fun x => T x ξ) μ := by
…

theorem OAI.KadisonKastler.operator_field_aestronglyMeasurable_of_dense_coefficients line 95

Source documentation

The two sets of measurable evaluations needed for the weak operator field C-star algebra follow from the same countable coefficient data.

theorem operator_field_aestronglyMeasurable_of_dense_coefficients [Countable ι]
    (v : ι → H) (hv : DenseRange v) (T : D → H →L[ℂ] H)
    (hT : ∀ i j, AEStronglyMeasurable (fun x => inner ℂ (v i) (T x (v j))) μ) :
    ∀ ξ, AEStronglyMeasurable (fun x => T x ξ) μ ∧
      AEStronglyMeasurable (fun x => star (T x) ξ) μ := by
…