FiniteDensityPowersStormer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional Powers–Størmer inequality with the error measured in the actual operator-predual norm. This is the norm supplied by the hypertrace separation argument.

def OAI.WeakPureInfiniteness.finiteOperatorTraceDensity line 18
lemma OAI.WeakPureInfiniteness.finiteOperatorTraceDensity_apply line 23
lemma OAI.WeakPureInfiniteness.trace_abs_le_predual_norm line 31
theorem OAI.WeakPureInfiniteness.finite_density_root_predual_bound line 47
Source documentation
The square roots of two positive density matrices differ in squared Hilbert–Schmidt norm by at most the norm of their difference as functionals.
```
theorem finite_density_root_predual_bound (h k : H →L[ℂ] H)
    (hh : 0 ≤ h) (hk : 0 ≤ k) :
    ‖NuclearUltrapower.finiteOperatorTensor (CFC.sqrt h) -
      NuclearUltrapower.finiteOperatorTensor (CFC.sqrt k)‖ ^ 2 ≤
      ‖finiteOperatorTraceDensity (h - k)‖ := by
…
```
Mentions: OAI.NuclearUltrapower.finiteOperatorTensor, OAI.WeakPureInfiniteness.finiteOperatorTraceDensity