OAI/Analysis/KadisonKastler/ProjectionStratumOperators.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.projectionRangeRestriction line 18

   Source documentation

   Restriction to an invariant projection range, retaining the original norm.

   def projectionRangeRestriction (P T : H →L[ℂ] H)
       (hT : ∀ v ∈ P.range, T v ∈ P.range) : P.range →L[ℂ] P.range :=
   …

2. theorem OAI.KadisonKastler.projectionRangeRestriction_coe line 23
3. theorem OAI.KadisonKastler.projectionRangeRestriction_norm_le line 28
4. def OAI.KadisonKastler.projectionStratumOperator line 39

   Source documentation

   An invariant operator field in a fixed Hilbert space on each rank stratum.

   def projectionStratumOperator (T : X → H →L[ℂ] H)
       (hT : ∀ x v, v ∈ (P x).range → T x v ∈ (P x).range)
       (n : ℕ) (x : projectionRankStratum P b n) :
       ℓ²(projectionDimensionIndex n, ℂ) →L[ℂ] ℓ²(projectionDimensionIndex n, ℂ) := by
   …

   Mentions: OAI.KadisonKastler.projectionRankStratum, OAI.KadisonKastler.projectionDimensionIndex

5. theorem OAI.KadisonKastler.projectionStratumOperator_apply line 48
6. theorem OAI.KadisonKastler.projectionStratumOperator_norm_le line 57
7. theorem OAI.KadisonKastler.projectionStratumOperator_measurable line 70