@[reducible, inline]

abbrev Orthogonalization.MvN.OrthAtN {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) (ι : Type u_1) [Fintype ι] : Prop

Theorem 1.2 at z for the functionals normal on M.

Equations

• Orthogonalization.MvN.OrthAtN M z ι = Orthogonalization.Blocks.OrthAtP M z ι (Orthogonalization.MvN.IsNormalOn M)

theorem Orthogonalization.MvN.IsNormalOn.smul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (h : IsNormalOn M φ) (c : ℂ) : IsNormalOn M (c • φ)

theorem Orthogonalization.MvN.NormalState.isNormalOn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (φ : NormalState M) : IsNormalOn M φ.toLinearMap

theorem Orthogonalization.MvN.orthAtN_one_of_blocks {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {κ : Type u_1} [Fintype κ] (z : κ → H →L[ℂ] H) (hz : ∀ (j : κ), Blocks.IsCentralProj M (z j)) (hzo : ∀ (j k : κ), j ≠ k → z j * z k = 0) (hzs : ∑ j : κ, z j = 1) (ι : Type u_2) [Fintype ι] (h : ∀ (j : κ), OrthAtN M (z j) ι) : OrthAtN M 1 ι

Gluing for normal functionals (Blocks/Glue.lean).

The weighted triangle inequality for functionals positive on M

theorem Orthogonalization.MvN.re_map_star_add_mul_add_le {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {x y : H →L[ℂ] H} (hx : x ∈ M) (hy : y ∈ M) {s : ℝ} (hs : 0 < s) : (φ (star (x + y) * (x + y))).re ≤ (1 + s) * (φ (star x * x)).re + (1 + s⁻¹) * (φ (star y * y)).re

φ(|x + y|²) ≤ (1 + s) φ(|x|²) + (1 + s⁻¹) φ(|y|²) for x, y ∈ M, s > 0, and φ positive on M: from 0 ≤ φ(|s x − y|²).

theorem Orthogonalization.MvN.sum_re_map_star_add_mul_add_le {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {ι : Type u_1} [Fintype ι] {x y : ι → H →L[ℂ] H} (hx : ∀ (i : ι), x i ∈ M) (hy : ∀ (i : ι), y i ∈ M) {s : ℝ} (hs : 0 < s) : (φ (∑ i : ι, star (x i + y i) * (x i + y i))).re ≤ (1 + s) * (φ (∑ i : ι, star (x i) * x i)).re + (1 + s⁻¹) * (φ (∑ i : ι, star (y i) * y i)).re

The tuple form of the weighted triangle inequality.

Lemma 4.1: normal functionals along bounded strongly convergent nets

theorem Orthogonalization.MvN.IsNormalOn.tendsto_re {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : IsNormalOn M φ) {κ : Type u} {l : Filter κ} {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} (hT : ∀ (k : κ), T k ∈ M) (hL : L ∈ M) (h : CommutingRepetition.VN.TendstoStrongBdd l T L) : Filter.Tendsto (fun (k : κ) => (φ (T k)).re) l (nhds (φ L).re)

theorem CommutingRepetition.VN.TendstoStrongBdd.sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} {T S : κ → H →L[ℂ] H} {L L' : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (h' : TendstoStrongBdd l S L') : TendstoStrongBdd l (fun (i : κ) => T i - S i) (L - L')

theorem CommutingRepetition.VN.TendstoStrongBdd.finset_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} {γ : Type u_3} (s : Finset γ) {T : γ → κ → H →L[ℂ] H} {L : γ → H →L[ℂ] H} (h : ∀ j ∈ s, TendstoStrongBdd l (T j) (L j)) : TendstoStrongBdd l (fun (i : κ) => ∑ j ∈ s, T j i) (∑ j ∈ s, L j)