ReducedDensityPredual.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite tensor vectors give actual finite vector functionals. Their norm controls the distance of their reduced-density square roots, without a dimension bound on the ambient Hilbert spaces.

def OAI.WeakPureInfiniteness.tensorActionOnVector line 18
def OAI.WeakPureInfiniteness.tensorCoefficient line 28
lemma OAI.WeakPureInfiniteness.tensorCoefficient_apply line 32
lemma OAI.WeakPureInfiniteness.tensorCoefficient_mem line 38
def OAI.WeakPureInfiniteness.finiteTensorDensity line 64
lemma OAI.WeakPureInfiniteness.finiteTensorDensity_apply line 68
lemma OAI.WeakPureInfiniteness.finiteTensorDensity_trace line 73
lemma OAI.WeakPureInfiniteness.operatorLift_norm_le line 82
lemma OAI.WeakPureInfiniteness.finiteTensorDensity_operatorLift line 98
lemma OAI.WeakPureInfiniteness.finiteTensorDensity_lift_norm_le line 120
theorem OAI.WeakPureInfiniteness.densityRoot_predual_bound line 140
Source documentation
The predual norm estimate survives passage to the common finite support of the two densities. No ambient finite-dimensionality is assumed.
```
theorem densityRoot_predual_bound (z w : E ⊗[ℂ] H) :
    ‖NuclearUltrapower.densityRoot z - NuclearUltrapower.densityRoot w‖ ^ 2 ≤
      ‖finiteTensorDensity z - finiteTensorDensity w‖ := by
…
```
Mentions: OAI.NuclearUltrapower.densityRoot, OAI.WeakPureInfiniteness.finiteTensorDensity
lemma OAI.WeakPureInfiniteness.finiteTensorDensity_unitary line 173
theorem OAI.WeakPureInfiniteness.densityRoot_unitary_predual_bound line 194
Source documentation
Norm-small conjugation defects of a finite positive functional yield Hilbert–Schmidt-small conjugation defects of its positive square root.
```
theorem densityRoot_unitary_predual_bound (U : H ≃ₗᵢ[ℂ] H) (z : E ⊗[ℂ] H) :
    ‖NuclearUltrapower.hsConjugation U (NuclearUltrapower.densityRoot z) -
      NuclearUltrapower.densityRoot z‖ ^ 2 ≤
      ‖finitePredualUnitary U (finiteTensorDensity z) - finiteTensorDensity z‖ := by
…
```
Mentions: OAI.NuclearUltrapower.hsConjugation, OAI.NuclearUltrapower.densityRoot, OAI.WeakPureInfiniteness.finitePredualUnitary, OAI.WeakPureInfiniteness.finiteTensorDensity