FiniteVectorDensityTensor.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite positive functionals obtained by separation have explicit tensor-vector and positive Hilbert–Schmidt square-root realizations.

def OAI.WeakPureInfiniteness.finiteVectorDensityTensor line 17
lemma OAI.WeakPureInfiniteness.finiteVectorDensityTensor_functional line 22
lemma OAI.WeakPureInfiniteness.finiteVectorDensityTensor_norm_sq line 44
lemma OAI.WeakPureInfiniteness.finiteVectorDensityTensor_norm_le_one line 62
theorem OAI.WeakPureInfiniteness.finiteVectorDensity_root_central line 75
Source documentation
The hypertrace construction's norm-central finite functional yields an actual positive finite-rank density root with the same centrality bound.
```
theorem finiteVectorDensity_root_central (w : Fin n → ℝ) (hw : ∀ k, 0 ≤ w k)
    (x : Fin n → H) (U : H ≃ₗᵢ[ℂ] H) :
    ‖NuclearUltrapower.hsConjugation U
        (NuclearUltrapower.densityRoot (finiteVectorDensityTensor w x)) -
      NuclearUltrapower.densityRoot (finiteVectorDensityTensor w x)‖ ^ 2 ≤
      ‖finitePredualUnitary U (finiteVectorDensity w x) - finiteVectorDensity w x‖ := by
…
```
Mentions: OAI.NuclearUltrapower.hsConjugation, OAI.NuclearUltrapower.densityRoot, OAI.WeakPureInfiniteness.finiteVectorDensityTensor, OAI.WeakPureInfiniteness.finitePredualUnitary, OAI.WeakPureInfiniteness.finiteVectorDensity