HilbertSchmidt.lean`

87 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.NuclearUltrapower.strongDualInner line 18
Source documentation
The conjugate Hilbert space realized as the strong dual. Its norm is the existing dual norm, not a new norm on the same space.
```
instance strongDualInner : InnerProductSpace ℂ (StrongDual ℂ K) where
…
```
theorem OAI.NuclearUltrapower.dual_inner_toDual line 27
def OAI.NuclearUltrapower.tensorOperator line 34
Source documentation
Algebraic finite-rank operators represented by Hilbert tensors.
```
def tensorOperator : K ⊗[ℂ] StrongDual ℂ K →ₗ[ℂ] (K →L[ℂ] K) :=
…
```
theorem OAI.NuclearUltrapower.tensorOperator_tmul line 44
theorem OAI.NuclearUltrapower.tensorOperator_inner line 48
Source documentation
Matrix coefficient identity, valid without any countability restriction.
```
theorem tensorOperator_inner (z : K ⊗[ℂ] StrongDual ℂ K) (v y : K) :
    ⟪y, tensorOperator z v⟫_ℂ = ⟪y ⊗ₜ[ℂ] InnerProductSpace.toDual ℂ K v, z⟫_ℂ := by
…
```
Mentions: OAI.NuclearUltrapower.tensorOperator
theorem OAI.NuclearUltrapower.tensorOperator_norm_le line 57
Source documentation
The operator norm is bounded by the Hilbert tensor (Hilbert--Schmidt) norm.
```
theorem tensorOperator_norm_le (z : K ⊗[ℂ] StrongDual ℂ K) :
    ‖tensorOperator z‖ ≤ ‖z‖ := by
…
```
Mentions: OAI.NuclearUltrapower.tensorOperator
instance OAI.NuclearUltrapower.tensorBoundedSMul line 73
Source comment
A shortcut for instance synthesis through the tensor's core norm.
```
instance tensorBoundedSMul : IsBoundedSMul ℂ (K ⊗[ℂ] StrongDual ℂ K) :=
…
```

abbrev OAI.NuclearUltrapower.HilbertSchmidt line 77

Source documentation

Hilbert--Schmidt vectors, with the actual tensor Hilbert norm.

abbrev HilbertSchmidt (K : Type*) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] := UniformSpace.Completion (K ⊗[ℂ] StrongDual ℂ K)

def OAI.NuclearUltrapower.tensorOperatorL line 80
def OAI.NuclearUltrapower.hsOperator line 90
Source documentation
Faithful operator realization of the Hilbert--Schmidt completion.
```
def hsOperator : HilbertSchmidt K →L[ℂ] (K →L[ℂ] K) :=
…
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt
theorem OAI.NuclearUltrapower.hsOperator_coe line 93
theorem OAI.NuclearUltrapower.hsOperator_tmul line 101
theorem OAI.NuclearUltrapower.hsOperator_compact line 106
Source documentation
All Hilbert--Schmidt operators are compact, without a separability assumption.
```
theorem hsOperator_compact (z : HilbertSchmidt K) : IsCompactOperator (hsOperator z) := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator

theorem OAI.NuclearUltrapower.hsOperator_inner line 123

Source documentation

Matrix coefficients of the completed operator realization.

theorem hsOperator_inner (z : HilbertSchmidt K) (v y : K) :
    ⟪y, hsOperator z v⟫_ℂ =
      ⟪((y ⊗ₜ[ℂ] InnerProductSpace.toDual ℂ K v : K ⊗[ℂ] StrongDual ℂ K) :
        HilbertSchmidt K), z⟫_ℂ := by
…

Mentions: OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator

theorem OAI.NuclearUltrapower.hsOperator_injective line 137
Source documentation
The operator realization loses no Hilbert--Schmidt vector.
```
theorem hsOperator_injective : Function.Injective (hsOperator (K := K)) := by
…
```
Mentions: OAI.NuclearUltrapower.hsOperator
def OAI.NuclearUltrapower.dualUnitary line 160
Source documentation
The conjugate (contragredient) unitary on the strong dual.
```
def dualUnitary (u : K ≃ₗᵢ[ℂ] K) : StrongDual ℂ K ≃ₗᵢ[ℂ] StrongDual ℂ K :=
…
```
theorem OAI.NuclearUltrapower.dualUnitary_toDual line 163
theorem OAI.NuclearUltrapower.dualUnitary_apply line 167

def OAI.NuclearUltrapower.completionUnitary line 175

Source documentation

Extension of a linear isometry equivalence to metric completions.

def completionUnitary {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    [NormedAddCommGroup F] [NormedSpace ℂ F] (u : E ≃ₗᵢ[ℂ] F) :
    UniformSpace.Completion E ≃ₗᵢ[ℂ] UniformSpace.Completion F :=
…

theorem OAI.NuclearUltrapower.completionUnitary_coe line 183
def OAI.NuclearUltrapower.hsConjugation line 189
Source documentation
Conjugation is unitary for the Hilbert--Schmidt norm.
```
def hsConjugation (u : K ≃ₗᵢ[ℂ] K) : HilbertSchmidt K ≃ₗᵢ[ℂ] HilbertSchmidt K :=
…
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt
theorem OAI.NuclearUltrapower.hsConjugation_coe line 193
theorem OAI.NuclearUltrapower.hsOperator_conjugation line 199
Source documentation
The tensor unitary acts by actual operator conjugation.
```
theorem hsOperator_conjugation (u : K ≃ₗᵢ[ℂ] K) (z : HilbertSchmidt K) :
    hsOperator (hsConjugation u z) =
      (u : K →L[ℂ] K) * hsOperator z * (u.symm : K →L[ℂ] K) := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator, OAI.NuclearUltrapower.hsConjugation
def OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep line 216
Source documentation
The absence of nonzero finite-dimensional subrepresentations, without separability.
```
def HasNoFiniteDimensionalSubrep (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) : Prop :=
…
```
theorem OAI.NuclearUltrapower.compact_selfadjoint_commuting_eq_zero line 222
Source documentation
The compact-operator obstruction used in the tensor-norm formulation. This is the selfadjoint case; no dimension bound and no separability are used.
```
theorem compact_selfadjoint_commuting_eq_zero
    (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) (hσ : HasNoFiniteDimensionalSubrep σ)
    (T : K →L[ℂ] K) (hT : IsCompactOperator T) (hsym : T.IsSymmetric)
    (hcomm : ∀ g x, T (σ g x) = σ g (T x)) : T = 0 := by
…
```
Mentions: OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep
theorem OAI.NuclearUltrapower.compact_commuting_eq_zero line 238
Source documentation
Every compact operator in the commutant vanishes, not just selfadjoint ones. This discharges the compact-operator part of lem:weak-mixing-bound.
```
theorem compact_commuting_eq_zero
    (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) (hσ : HasNoFiniteDimensionalSubrep σ)
    (T : K →L[ℂ] K) (hT : IsCompactOperator T)
    (hcomm : ∀ g x, T (σ g x) = σ g (T x)) : T = 0 := by
…
```
Mentions: OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep
theorem OAI.NuclearUltrapower.hsConjugation_one line 260
theorem OAI.NuclearUltrapower.hsConjugation_mul line 267
def OAI.NuclearUltrapower.hsRepresentation line 277
Source documentation
The conjugation representation on all Hilbert--Schmidt operators.
```
def hsRepresentation (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) :
    Γ →* (HilbertSchmidt K ≃ₗᵢ[ℂ] HilbertSchmidt K) where
…
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt
theorem OAI.NuclearUltrapower.hsRepresentation_no_invariants line 285
Source documentation
Weak mixing excludes every invariant Hilbert--Schmidt vector, with no separability assumption. This is the invariant-vector step of the source bound.
```
theorem hsRepresentation_no_invariants (σ : Γ →* (K ≃ₗᵢ[ℂ] K))
    (hσ : HasNoFiniteDimensionalSubrep σ) (z : HilbertSchmidt K)
    (hz : ∀ g, hsRepresentation σ g z = z) : z = 0 := by
…
```
Mentions: OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep, OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsRepresentation
structure OAI.NuclearUltrapower.PositiveTrace line 308
Source documentation
A finite positive trace. This definition is used only for the finite-rank part of the Powers--Størmer argument; no trace is assumed in the main theorem.
```
structure PositiveTrace (A : Type*) [CStarAlgebra A] [PartialOrder A] where
…
```
instance OAI.NuclearUltrapower.PositiveTrace.(instance at line 315) line 315
theorem OAI.NuclearUltrapower.PositiveTrace.map_add line 317
theorem OAI.NuclearUltrapower.PositiveTrace.map_sub line 319
theorem OAI.NuclearUltrapower.PositiveTrace.map_zero line 321
theorem OAI.NuclearUltrapower.PositiveTrace.mul_nonneg line 326
Source documentation
Positivity of the trace pairing does not require the factors to commute.
```
theorem mul_nonneg (τ : PositiveTrace A) {a b : A} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    0 ≤ τ (a * b) := by
…
```
Mentions: OAI.NuclearUltrapower.PositiveTrace
theorem OAI.NuclearUltrapower.PositiveTrace.contraction_pair_le_abs line 342
Source documentation
Pairing a selfadjoint contraction with an element is bounded by its trace absolute value. This is the elementary dual trace-norm estimate needed below.
```
theorem contraction_pair_le_abs (τ : PositiveTrace A) {j d : A}
    (hjlo : -1 ≤ j) (hjhi : j ≤ 1) (hd : IsSelfAdjoint d) :
    τ (j * d) ≤ τ (CFC.abs d) := by
…
```
Mentions: OAI.NuclearUltrapower.PositiveTrace
theorem OAI.NuclearUltrapower.PositiveTrace.square_sub_le_abs_pair line 357
Source documentation
The lower estimate in the Powers--Størmer argument.
```
theorem square_sub_le_abs_pair (τ : PositiveTrace A) {x y : A}
    (hx : 0 ≤ x) (hy : 0 ≤ y) :
    τ ((x - y) * (x - y)) ≤ τ (CFC.abs (x - y) * (x + y)) := by
…
```
Mentions: OAI.NuclearUltrapower.PositiveTrace

theorem OAI.NuclearUltrapower.PositiveTrace.exists_sign_of_finite_spectrum line 377

Source documentation

The finite-spectrum sign of a selfadjoint element.

theorem exists_sign_of_finite_spectrum {f : A} (hf : IsSelfAdjoint f)
    (hs : (spectrum ℝ f).Finite) :
    ∃ j : A, -1 ≤ j ∧ j ≤ 1 ∧ j * f = CFC.abs f ∧ f * j = CFC.abs f ∧ ‖j‖ ≤ 1 := by
…

theorem OAI.NuclearUltrapower.PositiveTrace.powers_stormer_finite_spectrum line 417
Source documentation
Powers--Størmer for a finite positive trace and a finite-spectrum difference. This is the finite-rank analytic core, not yet the Hilbert--Schmidt theorem.
```
theorem powers_stormer_finite_spectrum (τ : PositiveTrace A) {x y : A}
    (hx : 0 ≤ x) (hy : 0 ≤ y) (hfinite : (spectrum ℝ (x - y)).Finite) :
    τ ((x - y) * (x - y)) ≤ τ (CFC.abs (x * x - y * y)) := by
…
```
Mentions: OAI.NuclearUltrapower.PositiveTrace
def OAI.NuclearUltrapower.matrixPositiveTrace line 441
Source documentation
The ordinary (unnormalized) matrix trace, restricted to its real part.
```
def matrixPositiveTrace (n : Type*) [Fintype n] [DecidableEq n] :
    PositiveTrace (Matrix n n ℂ) where
…
```
Mentions: OAI.NuclearUltrapower.PositiveTrace

theorem OAI.NuclearUltrapower.matrix_powers_stormer line 448

Source documentation

Matrix form of the square-root trace inequality, in every size.

theorem matrix_powers_stormer {n : Type*} [Fintype n] [DecidableEq n]
    {x y : Matrix n n ℂ} (hx : x.PosSemidef) (hy : y.PosSemidef) :
    (Matrix.trace ((x - y) * (x - y))).re ≤
      (Matrix.trace (CFC.abs (x * x - y * y))).re :=
…

def OAI.NuclearUltrapower.finiteOperatorTensor line 462
Source documentation
The finite-dimensional Hilbert tensor representing an operator.
```
def finiteOperatorTensor [FiniteDimensional ℂ K] (T : K →L[ℂ] K) :
    K ⊗[ℂ] StrongDual ℂ K :=
…
```
theorem OAI.NuclearUltrapower.tensorOperator_finiteOperatorTensor line 467

theorem OAI.NuclearUltrapower.finiteOperatorTensor_inner line 477

Source documentation

The Hilbert--Schmidt inner product equals the unnormalized operator trace.

theorem finiteOperatorTensor_inner [FiniteDimensional ℂ K]
    (T U : K →L[ℂ] K) :
    ⟪finiteOperatorTensor T, finiteOperatorTensor U⟫_ℂ =
      LinearMap.trace ℂ K ((star T * U).toLinearMap) := by
…

Mentions: OAI.NuclearUltrapower.finiteOperatorTensor

theorem OAI.NuclearUltrapower.finiteOperatorTensor_norm_sq line 490
Source documentation
All finite-dimensional operators have their actual Hilbert--Schmidt norm.
```
theorem finiteOperatorTensor_norm_sq [FiniteDimensional ℂ K] (T : K →L[ℂ] K) :
    ‖finiteOperatorTensor T‖ ^ 2 =
      (LinearMap.trace ℂ K ((star T * T).toLinearMap)).re := by
…
```
Mentions: OAI.NuclearUltrapower.finiteOperatorTensor
def OAI.NuclearUltrapower.operatorPositiveTrace line 497
Source documentation
The real part of the ordinary trace on finite-dimensional operators.
```
def operatorPositiveTrace [FiniteDimensional ℂ K] : PositiveTrace (K →L[ℂ] K) where
…
```
Mentions: OAI.NuclearUltrapower.PositiveTrace
theorem OAI.NuclearUltrapower.operator_finite_real_spectrum line 508
Source documentation
Finite-dimensional operator spectra are finite also as real spectra.
```
theorem operator_finite_real_spectrum [FiniteDimensional ℂ K] (T : K →L[ℂ] K) :
    (spectrum ℝ T).Finite := by
…
```
def OAI.NuclearUltrapower.dualIsometry line 521
Source documentation
Functorial conjugate Hilbert-space embedding.
```
def dualIsometry (f : F →ₗᵢ[ℂ] K) : StrongDual ℂ F →ₗᵢ[ℂ] StrongDual ℂ K :=
…
```
theorem OAI.NuclearUltrapower.dualIsometry_toDual line 525
def OAI.NuclearUltrapower.liftOperatorTensor line 531
Source documentation
Tensorial inclusion of finite-rank operators along a Hilbert-space isometry.
```
def liftOperatorTensor (f : F →ₗᵢ[ℂ] K) [FiniteDimensional ℂ F] (T : F →L[ℂ] F) :
    K ⊗[ℂ] StrongDual ℂ K :=
…
```
theorem OAI.NuclearUltrapower.liftOperatorTensor_norm line 535

theorem OAI.NuclearUltrapower.tensorOperator_liftOperatorTensor line 540

Source documentation

This inclusion is the usual compression along an isometric embedding.

theorem tensorOperator_liftOperatorTensor (f : F →ₗᵢ[ℂ] K) [FiniteDimensional ℂ F]
    (T : F →L[ℂ] F) :
    tensorOperator (liftOperatorTensor f T) =
      f.toContinuousLinearMap ∘L T ∘L f.toContinuousLinearMap.adjoint := by
…

Mentions: OAI.NuclearUltrapower.tensorOperator, OAI.NuclearUltrapower.liftOperatorTensor

def OAI.NuclearUltrapower.crossOperator line 564
Source documentation
The rectangular operator associated with an algebraic Hilbert tensor.
```
def crossOperator : E ⊗[ℂ] K →ₗ[ℂ] (StrongDual ℂ E →L[ℂ] K) :=
…
```
theorem OAI.NuclearUltrapower.crossOperator_tmul line 574
theorem OAI.NuclearUltrapower.crossOperator_tmul_rankOne line 578
def OAI.NuclearUltrapower.reducedDensity line 585
Source documentation
The finite-rank reduced density; independent of any chosen tensor expansion.
```
def reducedDensity (z : E ⊗[ℂ] K) : K →L[ℂ] K :=
…
```
theorem OAI.NuclearUltrapower.reducedDensity_nonneg line 588

theorem OAI.NuclearUltrapower.trace_crossOperator line 593

Source documentation

The polarized partial-trace formula, before completion.

theorem trace_crossOperator [FiniteDimensional ℂ K] (z w : E ⊗[ℂ] K) (C : K →L[ℂ] K) :
    LinearMap.trace ℂ K ((C ∘L crossOperator z ∘L (crossOperator w).adjoint).toLinearMap) =
      ⟪w, TensorProduct.mapL (ContinuousLinearMap.id ℂ E) C z⟫_ℂ := by
…

Mentions: OAI.NuclearUltrapower.crossOperator

theorem OAI.NuclearUltrapower.trace_reducedDensity line 614

Source documentation

The reduced-density characterization by its trace.

theorem trace_reducedDensity [FiniteDimensional ℂ K] (z : E ⊗[ℂ] K) (C : K →L[ℂ] K) :
    LinearMap.trace ℂ K ((C * reducedDensity z).toLinearMap) =
      ⟪z, TensorProduct.mapL (ContinuousLinearMap.id ℂ E) C z⟫_ℂ :=
…

Mentions: OAI.NuclearUltrapower.reducedDensity

def OAI.NuclearUltrapower.operatorLift line 620
Source documentation
Conjugation/compression by an isometric Hilbert-space embedding.
```
def operatorLift (f : F →ₗᵢ[ℂ] K) (T : F →L[ℂ] F) : K →L[ℂ] K :=
…
```
theorem OAI.NuclearUltrapower.operatorLift_mul line 623
theorem OAI.NuclearUltrapower.operatorLift_nonneg line 632
theorem OAI.NuclearUltrapower.operatorLift_sqrt line 637

theorem OAI.NuclearUltrapower.crossOperator_mapIsometry line 648

Source documentation

Naturality of the rectangular operator under arbitrary isometric embeddings.

theorem crossOperator_mapIsometry (g : E →ₗᵢ[ℂ] E') (f : F →ₗᵢ[ℂ] K) (z : E ⊗[ℂ] F) :
    crossOperator (TensorProduct.mapIsometry g f z) =
      f.toContinuousLinearMap ∘L crossOperator z ∘L (dualIsometry g).toContinuousLinearMap.adjoint := by
…

Mentions: OAI.NuclearUltrapower.crossOperator, OAI.NuclearUltrapower.dualIsometry

theorem OAI.NuclearUltrapower.reducedDensity_mapIsometry line 665
Source documentation
Partial trace discards an isometry on the first tensor factor.
```
theorem reducedDensity_mapIsometry (g : E →ₗᵢ[ℂ] E') (f : F →ₗᵢ[ℂ] K) (z : E ⊗[ℂ] F) :
    reducedDensity (TensorProduct.mapIsometry g f z) = operatorLift f (reducedDensity z) := by
…
```
Mentions: OAI.NuclearUltrapower.reducedDensity, OAI.NuclearUltrapower.operatorLift
theorem OAI.NuclearUltrapower.trace_reducedDensity_self line 680
Source documentation
Finite-dimensional density trace equals the vector's squared norm.
```
theorem trace_reducedDensity_self [FiniteDimensional ℂ K] (z : E ⊗[ℂ] K) :
    (LinearMap.trace ℂ K (reducedDensity z).toLinearMap).re = ‖z‖ ^ 2 := by
…
```
Mentions: OAI.NuclearUltrapower.reducedDensity

theorem OAI.NuclearUltrapower.vectorState_difference_le line 691

Source documentation

Elementary vector-state estimate, valid without separability or completeness.

theorem vectorState_difference_le (A : H →L[ℂ] H) (hA : ‖A‖ ≤ 1) (x y : H) :
    (⟪x, A x⟫_ℂ - ⟪y, A y⟫_ℂ).re ≤ (‖x‖ + ‖y‖) * ‖x - y‖ := by
…

theorem OAI.NuclearUltrapower.finiteOperatorTensor_sub line 713

theorem OAI.NuclearUltrapower.trace_abs_reducedDensity_sub_le line 720

Source documentation

The trace-norm estimate for reduced density matrices.

theorem trace_abs_reducedDensity_sub_le [FiniteDimensional ℂ K] (z w : E ⊗[ℂ] K) :
    (LinearMap.trace ℂ K (CFC.abs (reducedDensity z - reducedDensity w)).toLinearMap).re ≤
      (‖z‖ + ‖w‖) * ‖z - w‖ := by
…

Mentions: OAI.NuclearUltrapower.reducedDensity

theorem OAI.NuclearUltrapower.finite_density_root_difference line 736

Source documentation

Finite-dimensional Powers--Størmer in the Hilbert tensor norm.

theorem finite_density_root_difference [FiniteDimensional ℂ K] (z w : E ⊗[ℂ] K) :
    ‖finiteOperatorTensor (CFC.sqrt (reducedDensity z)) -
      finiteOperatorTensor (CFC.sqrt (reducedDensity w))‖ ^ 2 ≤
      (‖z‖ + ‖w‖) * ‖z - w‖ := by
…

Mentions: OAI.NuclearUltrapower.finiteOperatorTensor, OAI.NuclearUltrapower.reducedDensity

theorem OAI.NuclearUltrapower.finite_density_root_norm_sq line 754
Source documentation
The root of a finite-rank density has squared Hilbert--Schmidt norm equal exactly to the vector's squared Hilbert norm.
```
theorem finite_density_root_norm_sq [FiniteDimensional ℂ K] (z : E ⊗[ℂ] K) :
    ‖finiteOperatorTensor (CFC.sqrt (reducedDensity z))‖ ^ 2 = ‖z‖ ^ 2 := by
…
```
Mentions: OAI.NuclearUltrapower.finiteOperatorTensor, OAI.NuclearUltrapower.reducedDensity
theorem OAI.NuclearUltrapower.exists_density_root line 761
Source documentation
Every algebraic tensor has a genuine Hilbert--Schmidt reduced-density root, without any dimension or separability assumption on the ambient spaces.
```
theorem exists_density_root (z : E ⊗[ℂ] K) :
    ∃ a : HilbertSchmidt K, hsOperator a = CFC.sqrt (reducedDensity z) ∧ ‖a‖ = ‖z‖ := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator, OAI.NuclearUltrapower.reducedDensity
def OAI.NuclearUltrapower.densityRoot line 787
Source documentation
The unique Hilbert--Schmidt vector realizing the positive density root.
```
def densityRoot (z : E ⊗[ℂ] K) : HilbertSchmidt K := (exists_density_root z).choose
```
Mentions: OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.exists_density_root
theorem OAI.NuclearUltrapower.hsOperator_densityRoot line 789
theorem OAI.NuclearUltrapower.densityRoot_norm line 793
theorem OAI.NuclearUltrapower.densityRoot_mapIsometry line 797
Source documentation
Uniqueness makes the finite-support construction independent of all choices.
```
theorem densityRoot_mapIsometry [FiniteDimensional ℂ F]
    (g : E →ₗᵢ[ℂ] E') (f : F →ₗᵢ[ℂ] K) (z : E ⊗[ℂ] F) :
    densityRoot (TensorProduct.mapIsometry g f z) =
      (liftOperatorTensor f (CFC.sqrt (reducedDensity z)) : HilbertSchmidt K) := by
…
```
Mentions: OAI.NuclearUltrapower.densityRoot, OAI.NuclearUltrapower.liftOperatorTensor, OAI.NuclearUltrapower.reducedDensity, OAI.NuclearUltrapower.HilbertSchmidt
theorem OAI.NuclearUltrapower.liftOperatorTensor_sub line 806
theorem OAI.NuclearUltrapower.densityRoot_difference line 813
Source documentation
The reduced-root estimate holds in arbitrary ambient Hilbert spaces. Both vectors are compared inside one finite-dimensional support, not separately.
```
theorem densityRoot_difference (z w : E ⊗[ℂ] K) :
    ‖densityRoot z - densityRoot w‖ ^ 2 ≤ (‖z‖ + ‖w‖) * ‖z - w‖ := by
…
```
Mentions: OAI.NuclearUltrapower.densityRoot
theorem OAI.NuclearUltrapower.densityRoot_unitary line 830
Source documentation
Unitary covariance of reduced densities, realized in actual HS space.
```
theorem densityRoot_unitary (u : E ≃ₗᵢ[ℂ] E) (v : K ≃ₗᵢ[ℂ] K) (z : E ⊗[ℂ] K) :
    densityRoot (TensorProduct.congrIsometry u v z) = hsConjugation v (densityRoot z) := by
…
```
Mentions: OAI.NuclearUltrapower.densityRoot, OAI.NuclearUltrapower.hsConjugation

theorem OAI.NuclearUltrapower.densityRoot_unitary_difference line 843

Source documentation

The exact factor two in the Powers--Størmer inequality.

theorem densityRoot_unitary_difference (u : E ≃ₗᵢ[ℂ] E) (v : K ≃ₗᵢ[ℂ] K)
    (z : E ⊗[ℂ] K) :
    ‖hsConjugation v (densityRoot z) - densityRoot z‖ ^ 2 ≤
      (2 * ‖z‖) * ‖TensorProduct.congrIsometry u v z - z‖ := by
…

Mentions: OAI.NuclearUltrapower.hsConjugation, OAI.NuclearUltrapower.densityRoot

def OAI.NuclearUltrapower.HasKazhdanGap line 852
Source documentation
Exact standing Kazhdan-gap convention in the tensor-norm formulation.
```
def HasKazhdanGap {Γ : Type u} [Group Γ] (S : Finset Γ) (κ : ℝ) : Prop :=
…
```

theorem OAI.NuclearUltrapower.weak_mixing_bound_algebraic line 859

Source documentation

The full weak-mixing estimate on the dense algebraic tensor product.

theorem weak_mixing_bound_algebraic {Γ : Type u} [Group Γ]
    (S : Finset Γ) (κ : ℝ) (hS : S.Nonempty) (hκ : 0 < κ)
    (hgap : HasKazhdanGap.{u, v} S κ)
    {K : Type v} {E : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) (hσ : HasNoFiniteDimensionalSubrep σ)
    (U : Γ → (E ≃ₗᵢ[ℂ] E)) (z : E ⊗[ℂ] K) :
    κ ^ 2 / (4 * (S.card : ℝ)) * ‖z‖ ^ 2 ≤
      ∑ s ∈ S, ‖TensorProduct.congrIsometry (U s) (σ s) z - z‖ ^ 2 := by
…

Mentions: OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep

abbrev OAI.NuclearUltrapower.HilbertTensor line 896

def OAI.NuclearUltrapower.tensorUnitaryAction line 901

Source documentation

Exact completed tensor action used in the source uniform spectral bound.

def tensorUnitaryAction {E K : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℂ E] [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    (u : E ≃ₗᵢ[ℂ] E) (v : K ≃ₗᵢ[ℂ] K) :
    HilbertTensor E K →L[ℂ] HilbertTensor E K :=
…

Mentions: OAI.NuclearUltrapower.HilbertTensor

theorem OAI.NuclearUltrapower.tensorUnitaryAction_coe line 908

theorem OAI.NuclearUltrapower.weak_mixing_bound line 919

Source documentation

Source lem:weak-mixing-bound, for arbitrary (possibly nonseparable) Hilbert spaces and arbitrary unitaries U_s with no relations imposed.

theorem weak_mixing_bound {Γ : Type u} [Group Γ]
    (S : Finset Γ) (κ : ℝ) (hS : S.Nonempty) (hκ : 0 < κ)
    (hgap : HasKazhdanGap.{u, v} S κ)
    {K : Type v} {E : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) (hσ : HasNoFiniteDimensionalSubrep σ)
    (U : Γ → (E ≃ₗᵢ[ℂ] E)) (ξ : HilbertTensor E K) :
    κ ^ 2 / (4 * (S.card : ℝ)) * ‖ξ‖ ^ 2 ≤
      ∑ s ∈ S, ‖tensorUnitaryAction (U s) (σ s) ξ - ξ‖ ^ 2 := by
…

Mentions: OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep, OAI.NuclearUltrapower.HilbertTensor, OAI.NuclearUltrapower.tensorUnitaryAction