HilbertSchmidtUnitaryActions.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Left and right unitary actions on Hilbert–Schmidt vectors. The conjugation estimate gives the actual left/right intertwining estimate.

def OAI.WeakPureInfiniteness.hsLeftUnitary line 15
def OAI.WeakPureInfiniteness.hsRightUnitary line 21
lemma OAI.WeakPureInfiniteness.hsRight_conjugation line 27
lemma OAI.WeakPureInfiniteness.hsLeft_sub_right_norm line 49
theorem OAI.WeakPureInfiniteness.densityRoot_left_right_bound line 56
Source documentation
The square root of a nearly central finite density is an actual approximate intertwiner for the left and right unitary actions.
```
theorem densityRoot_left_right_bound {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℂ E] [CompleteSpace E] (U : H ≃ₗᵢ[ℂ] H) (z : E ⊗[ℂ] H) :
    ‖hsLeftUnitary U (NuclearUltrapower.densityRoot z) -
      hsRightUnitary U (NuclearUltrapower.densityRoot z)‖ ^ 2 ≤
      ‖finitePredualUnitary U (finiteTensorDensity z) - finiteTensorDensity z‖ := by
…
```
Mentions: OAI.WeakPureInfiniteness.hsLeftUnitary, OAI.NuclearUltrapower.densityRoot, OAI.WeakPureInfiniteness.hsRightUnitary, OAI.WeakPureInfiniteness.finitePredualUnitary, OAI.WeakPureInfiniteness.finiteTensorDensity