Separable quantum state

import Quantum_state
import rnd_var

/-- Separable quantum state -/
def separable [quantum_state ρ] := 
∃ (px : ι → ℝ) [rnd_var px] [ρx σx : ι → quantum_state], 
∑ i, (px i) * (ρx i) ⊗ (σx i) = ρ

/--
Another form
https://arxiv.org/abs/2111.02438
"States composed of all those states σ admitting a decomposition of the form
...
where \mu \nu are appropriate meaures on the set of pure states.
"
-/
def separable' [quantum_state ρ] := sorry

Positive partial transpose of separable state;