MeasurableFieldAdjoint.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Adjoint and projection laws for bounded measurable fields

Pointwise adjoint laws pass to the actual L² operators by integrating the Hilbert inner-product identity. In particular, a measurable field of orthogonal projections defines an actual orthogonal projection on L².

theorem OAI.KadisonSimilarity.boundedFieldOperator_eq_adjoint_of_ae line 20

Source documentation

A pointwise adjoint field constructs the actual Hilbert-space adjoint.

theorem boundedFieldOperator_eq_adjoint_of_ae
    (R S : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (hS : ∀ x : H, AEStronglyMeasurable (fun a => S a x) μ)
    (C D : ℝ) (hRbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C) (hSbound : ∀ᵐ a ∂μ, ‖S a‖ ≤ D)
    (hadjoint : ∀ᵐ a ∂μ, S a = star (R a)) :
    boundedFieldOperator μ S hS D hSbound =
      (boundedFieldOperator μ R hR C hRbound).adjoint := by
…

Mentions: OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.boundedFieldOperator_isSelfAdjoint line 39

Source documentation

Almost-everywhere selfadjointness of the field yields a selfadjoint bounded L² operator.

theorem boundedFieldOperator_isSelfAdjoint
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (hself : ∀ᵐ a ∂μ, IsSelfAdjoint (R a)) :
    IsSelfAdjoint (boundedFieldOperator μ R hR C hbound) := by
…

Mentions: OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.boundedFieldOperator_isIdempotentElem line 53

Source documentation

Almost-everywhere idempotence passes to the actual operator by its pointwise action on every L² vector.

theorem boundedFieldOperator_isIdempotentElem
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (hidem : ∀ᵐ a ∂μ, IsIdempotentElem (R a)) :
    IsIdempotentElem (boundedFieldOperator μ R hR C hbound) :=
…

Mentions: OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.boundedFieldOperator_isStarProjection line 64

Source documentation

The reverse field construction preserves orthogonal projections.

theorem boundedFieldOperator_isStarProjection
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (hproj : ∀ᵐ a ∂μ, IsStarProjection (R a)) :
    IsStarProjection (boundedFieldOperator μ R hR C hbound) where
…

Mentions: OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.measurableProjection_norm_bound line 77

Source documentation

The uniform bound needed for a field of orthogonal projections follows from the projection equations themselves.

theorem measurableProjection_norm_bound
    (p : Ω → H →L[ℂ] H) (hp : ∀ᵐ a ∂μ, IsStarProjection (p a)) :
    ∀ᵐ a ∂μ, ‖p a‖ ≤ 1 := hp.mono fun _ ha => IsStarProjection.norm_le _ ha

def OAI.KadisonSimilarity.measurableProjectionOperator line 83

Source documentation

An actual orthogonal projection from a strongly measurable projection field; no separate uniform-bound hypothesis is required.

def measurableProjectionOperator
    (p : Ω → H →L[ℂ] H)
    (hmeas : ∀ x : H, AEStronglyMeasurable (fun a => p a x) μ)
    (hp : ∀ᵐ a ∂μ, IsStarProjection (p a)) : Lp H 2 μ →L[ℂ] Lp H 2 μ :=
…

theorem OAI.KadisonSimilarity.measurableProjectionOperator_isStarProjection line 89
theorem OAI.KadisonSimilarity.measurableProjectionOperator_action line 97
theorem OAI.KadisonSimilarity.measurableProjectionOperator_norm_le line 104