ProjectionRankOne.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Supported rank-one fields supply countably many tests for the full operator algebra on each projection range. Their bounds and measurability follow from the projection columns themselves.

theorem OAI.KadisonSimilarity.projection_rankOne_support line 18

Source documentation

A rank-one operator with both vectors in a projection range is supported on that range on both sides.

theorem projection_rankOne_support (p : H →L[ℂ] H) (hp : IsStarProjection p)
    (v w : H) :
    p * InnerProductSpace.rankOne ℂ (p v) (p w) =
        InnerProductSpace.rankOne ℂ (p v) (p w) ∧
      InnerProductSpace.rankOne ℂ (p v) (p w) * p =
        InnerProductSpace.rankOne ℂ (p v) (p w) := by
…

theorem OAI.KadisonSimilarity.projectionFiberCompression_rankOne line 39

Source documentation

Compression gives the ordinary rank-one operator on the range.

theorem projectionFiberCompression_rankOne (p : H →L[ℂ] H) (hp : IsStarProjection p)
    (v w : H) :
    projectionFiberCompression p hp (InnerProductSpace.rankOne ℂ (p v) (p w)) =
      InnerProductSpace.rankOne ℂ (projectionFiberRetraction p hp v)
        (projectionFiberRetraction p hp w) := by
…

Mentions: OAI.KadisonSimilarity.projectionFiberCompression, OAI.KadisonSimilarity.projectionFiberRetraction

theorem OAI.KadisonSimilarity.norm_projection_apply_le line 51
theorem OAI.KadisonSimilarity.norm_projection_rankOne_le line 59

theorem OAI.KadisonSimilarity.aestronglyMeasurable_projection_rankOne line 70

Source documentation

Strongly measurable projection columns give strongly measurable columns for every supported rank-one field.

theorem aestronglyMeasurable_projection_rankOne
    (p : Ω → H →L[ℂ] H)
    (hmeas : ∀ v : H, AEStronglyMeasurable (fun a => p a v) μ) (v w x : H) :
    AEStronglyMeasurable
      (fun a => InnerProductSpace.rankOne ℂ (p a v) (p a w) x) μ := by
…