CyclicSummandColumns.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Finite column implementers from an actual orthogonal decomposition into reducing summands. The finite projections converge strongly by density.

structure OAI.KadisonSimilarity.OrthogonalSummandDecomposition line 22
Source documentation
Isometric summand inclusions with mutually orthogonal ranges and dense linear span. The summands may have different Hilbert spaces.
```
structure OrthogonalSummandDecomposition (K : I → Type*)
    [∀ i, NormedAddCommGroup (K i)] [∀ i, InnerProductSpace ℂ (K i)]
    (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] where
…
```

def OAI.KadisonSimilarity.OrthogonalSummandDecomposition.of_adjoint_orthogonal line 34

Source documentation

Construct the geometric decomposition from the operator form of orthogonality of the inclusions.

def of_adjoint_orthogonal (U : ∀ i, K i →ₗᵢ[ℂ] H)
    (horth : ∀ i j, i ≠ j →
      (U i).toContinuousLinearMap.adjoint.comp (U j).toContinuousLinearMap = 0)
    (hdense : (Submodule.span ℂ (⋃ i, Set.range (U i))).topologicalClosure = ⊤) :
    OrthogonalSummandDecomposition K H where
…

Mentions: OAI.KadisonSimilarity.OrthogonalSummandDecomposition

def OAI.KadisonSimilarity.OrthogonalSummandDecomposition.coordinate line 50
def OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection line 53
Source documentation
The projection onto any finite collection of summands.
```
def finiteProjection (F : Finset I) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.coordinate_inclusion_self line 56
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.coordinate_inclusion_ne line 60
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection_apply line 68
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.coordinate_finiteProjection line 72
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection_idempotent line 90
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection_adjoint line 100
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.norm_finiteProjection_le_one line 105
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection_inclusion line 113
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection_eventually_fixed line 124
Source documentation
Every vector in the algebraic span is fixed by all sufficiently large finite summand projections.
```
theorem finiteProjection_eventually_fixed (x : H)
    (hx : x ∈ Submodule.span ℂ (⋃ i, Set.range (U.inclusion i))) :
    ∃ F₀ : Finset I, ∀ F, F₀ ⊆ F → U.finiteProjection F x = x := by
…
```
theorem OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection_tendsto line 144
Source documentation
Finite orthogonal sums converge strongly to the identity on the completed space; only the dense linear span is used.
```
theorem finiteProjection_tendsto (x : H) :
    Tendsto (fun F : Finset I => U.finiteProjection F x) atTop (𝓝 x) := by
…
```

def OAI.KadisonSimilarity.finiteColumnImplementers_of_summands line 183

Source documentation

Actual finite-column implementers obtained from implemented restrictions to the summands. Cyclicity is used to obtain the local implementers, not in their assembly.

def finiteColumnImplementers_of_summands
    (U : OrthogonalSummandDecomposition K H)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (σi : ∀ i, A →⋆ₐ[ℂ] (K i →L[ℂ] K i))
    (δ : A →L[ℂ] (H →L[ℂ] H)) (V : ∀ i, K i →L[ℂ] H)
    (hσ : ∀ i a, (σ a).comp (U.inclusion i).toContinuousLinearMap =
      (U.inclusion i).toContinuousLinearMap.comp (σi i a))
    (hV : ∀ i a, (δ a).comp (U.inclusion i).toContinuousLinearMap =
      (V i).comp (σi i a) - (σ a).comp (V i)) :
    FiniteColumnImplementers σ δ (atTop : Filter (Finset I)) where
…

Mentions: OAI.KadisonSimilarity.OrthogonalSummandDecomposition, OAI.KadisonSimilarity.FiniteColumnImplementers

theorem OAI.KadisonSimilarity.derivation_completeBound_of_implemented_summands line 218

Source documentation

The uniform commutator estimate bounds a derivation on a dense orthogonal family of implemented reducing summands.

theorem derivation_completeBound_of_implemented_summands
    (U : OrthogonalSummandDecomposition K H)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (σi : ∀ i, A →⋆ₐ[ℂ] (K i →L[ℂ] K i))
    (δ : A →L[ℂ] (H →L[ℂ] H)) (V : ∀ i, K i →L[ℂ] H)
    (hσ : ∀ i a, (σ a).comp (U.inclusion i).toContinuousLinearMap =
      (U.inclusion i).toContinuousLinearMap.comp (σi i a))
    (hV : ∀ i a, (δ a).comp (U.inclusion i).toContinuousLinearMap =
      (V i).comp (σi i a) - (σ a).comp (V i))
    (P : VonNeumannAlgebra H) (hP : ∀ a, σ a ∈ P)
    (kaplansky : ScalarKaplanskyClosure σ P)
    {C : ℝ} (hC : 0 ≤ C) (estimate : CommutatorEstimate P C) :
    CompleteBound δ (C * ‖δ‖) :=
…

Mentions: OAI.KadisonSimilarity.OrthogonalSummandDecomposition, OAI.KadisonSimilarity.ScalarKaplanskyClosure, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.CompleteBound