OAI/Analysis/FiniteFactor/Diffuse/OperatorSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Nonhyperlinear.Diffuseness.rangeSupport line 13

   Source documentation

   The actual orthogonal projection onto the closed range of an operator.

   def rangeSupport (T : H →L[ℂ] H) : H →L[ℂ] H :=
   …

2. lemma OAI.Nonhyperlinear.Diffuseness.rangeSupport_projection line 16
3. lemma OAI.Nonhyperlinear.Diffuseness.rangeSupport_range line 19
4. lemma OAI.Nonhyperlinear.Diffuseness.rangeSupport_mul_self line 23
5. lemma OAI.Nonhyperlinear.Diffuseness.rangeSupport_ne_zero line 28
6. theorem OAI.Nonhyperlinear.Diffuseness.rangeSupport_mem line 35

   Source documentation

   Closed range support belongs to the same concrete von Neumann algebra.

   theorem rangeSupport_mem (M : VonNeumannAlgebra H) {T:H→L[ℂ]H} (hT:T∈M) :
       rangeSupport T∈M := by
   …

   Mentions: OAI.Nonhyperlinear.Diffuseness.rangeSupport

7. lemma OAI.Nonhyperlinear.Diffuseness.projection_mul_rangeSupport line 47
8. lemma OAI.Nonhyperlinear.Diffuseness.rangeSupport_mul_projection line 61