TraceFieldMeasurable.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable operator fields from their tracial Hilbert realizations

On an operator-norm bounded ball, trace two-norm convergence implies strong operator convergence. Thus a measurable trace-Hilbert field gives measurable Hilbert-valued evaluations in the original representation.

theorem OAI.KadisonKastler.continuous_traceBall_eval line 25

Source documentation

Strong-operator evaluation is continuous on a bounded trace-Hilbert ball.

theorem continuous_traceBall_eval (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) {C : ℝ} (hC : 0 ≤ C)
    (lift : (J '' Metric.closedBall (0 : Algebra M) C) → Algebra M)
    (hlift : ∀ z, J (lift z) = z.val ∧ ‖lift z‖ ≤ C) (ξ : H) :
    Continuous (fun z => (lift z : H →L[ℂ] H) ξ) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.aestronglyMeasurable_operator_eval_of_trace line 48

Source documentation

A globally bounded algebra field measurable in its trace Hilbert space is strongly measurable after evaluation at any Hilbert vector.

theorem aestronglyMeasurable_operator_eval_of_trace [SeparableSpace H]
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) {μ : Measure D}
    (a : D → Algebra M) {C : ℝ} (hC : 0 ≤ C) (ha : ∀ x, ‖a x‖ ≤ C)
    (hmeas : AEStronglyMeasurable (fun x => J (a x)) μ) (ξ : H) :
    AEStronglyMeasurable (fun x => (a x : H →L[ℂ] H) ξ) μ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.aestronglyMeasurable_operator_coefficient_of_trace line 75

Source documentation

In particular all scalar matrix coefficients are measurable.

theorem aestronglyMeasurable_operator_coefficient_of_trace [SeparableSpace H]
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) {μ : Measure D}
    (a : D → Algebra M) {C : ℝ} (hC : 0 ≤ C) (ha : ∀ x, ‖a x‖ ≤ C)
    (hmeas : AEStronglyMeasurable (fun x => J (a x)) μ) (ξ η : H) :
    AEStronglyMeasurable (fun x => inner ℂ η ((a x : H →L[ℂ] H) ξ)) μ :=
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace