SupportedFieldRecovery.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Supported measurable fields are recovered exactly by compression to the original Hilbert space. In particular, the supported rank-one tests used for factor fibers come from actual original operators.

theorem OAI.KadisonSimilarity.isometricExtension_boundedField_compression line 22

Source documentation

An operator field supported on the original range is exactly the zero extension of its compression.

theorem isometricExtension_boundedField_compression
    (p R : Ω → F →L[ℂ] F)
    (hP : ∀ f : Lp F 2 μ, ∀ᵐ x ∂μ, isometricExtension J 1 f x = p x (f x))
    (hmeas : ∀ v : F, AEStronglyMeasurable (fun x => R x v) μ)
    (C : ℝ) (hbound : ∀ᵐ x ∂μ, ‖R x‖ ≤ C)
    (hleft : ∀ᵐ x ∂μ, p x * R x = R x)
    (hright : ∀ᵐ x ∂μ, R x * p x = R x) :
    isometricExtension J
      ((J.toContinuousLinearMap.adjoint.comp (boundedFieldOperator μ R hmeas C hbound)).comp
        J.toContinuousLinearMap) = boundedFieldOperator μ R hmeas C hbound :=
…

Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.aestronglyMeasurable_isometric_projection_column line 39

Source documentation

The projection columns of the original range are strongly measurable.

theorem aestronglyMeasurable_isometric_projection_column
    (p : Ω → F →L[ℂ] F)
    (hP : ∀ f : Lp F 2 μ, ∀ᵐ x ∂μ, isometricExtension J 1 f x = p x (f x))
    (v : F) : AEStronglyMeasurable (fun x => p x v) μ :=
…

Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.exists_isometric_projection_rankOne_field line 48

Source documentation

Every supported rank-one field is the field of an actual operator on the original Hilbert space.

theorem exists_isometric_projection_rankOne_field
    (p : Ω → F →L[ℂ] F) (hp : ∀ x, IsStarProjection (p x))
    (hP : ∀ f : Lp F 2 μ, ∀ᵐ x ∂μ, isometricExtension J 1 f x = p x (f x))
    (v w : F) :
    ∃ T : H →L[ℂ] H, ∀ f : Lp F 2 μ, ∀ᵐ x ∂μ,
      isometricExtension J T f x =
        InnerProductSpace.rankOne ℂ (p x v) (p x w) (f x) := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension