OAI/Analysis/KadisonKastler/DecreasingHilbertProjections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The strong limit of decreasing Hilbert projections

The squared norms decrease. Their Cauchy estimate identifies the strong limit with projection onto the intersection, as needed for central vectors.

  1. theorem OAI.KadisonKastler.decreasing_projection_limit line 23

    Source documentation

    Decreasing closed subspaces have strongly convergent projections.

    theorem decreasing_projection_limit (K : ℕ → Submodule ℂ H)
    [∀ n, CompleteSpace (K n)] (hK : Antitone K) (ξ : H) :
    ∃ η : H, (∀ n, η ∈ K n) ∧
      Tendsto (fun n => (K n).starProjection ξ) atTop (𝓝 η) ∧
      ∀ w : H, (∀ n, w ∈ K n) → inner ℂ (ξ - η) w = 0 := by
…