theorem
Orthogonalization.Blocks.star_sum_mul_sum
{κ : Type u_2}
[Fintype κ]
{A : Type u_3}
[NonUnitalNonAssocSemiring A]
[StarRing A]
(b : κ → A)
(h : ∀ (j k : κ), j ≠ k → star (b j) * b k = 0)
:
star (∑ b j) * ∑ b j = ∑ star (b j) * b j when the cross terms vanish.
def
Orthogonalization.Blocks.OrthAtP
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
(z : H →L[ℂ] H)
(ι : Type u_2)
[Fintype ι]
(P : ((H →L[ℂ] H) →ₗ[ℂ] ℂ) → Prop)
:
Theorem 1.2 at z for the functionals satisfying a predicate P (OrthAt M z ι
is the case P = fun _ => True; the normal functionals are the case of tier T3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Orthogonalization.Blocks.orthAtP_true_iff
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
(z : H →L[ℂ] H)
(ι : Type u_2)
[Fintype ι]
:
theorem
Orthogonalization.Blocks.orthAtP_one_of_blocks
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
{κ : Type u_2}
[Fintype κ]
(z : κ → H →L[ℂ] H)
(hz : ∀ (j : κ), IsCentralProj M (z j))
(hzo : ∀ (j k : κ), j ≠ k → z j * z k = 0)
(hzs : ∑ j : κ, z j = 1)
(ι : Type u_3)
[Fintype ι]
(P : ((H →L[ℂ] H) →ₗ[ℂ] ℂ) → Prop)
(hP : ∀ (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ), P φ → ∀ (c : ℝ), 0 < c → P (↑c • φ))
(h : ∀ (j : κ), OrthAtP M (z j) ι P)
:
OrthAtP M 1 ι P
Gluing. Theorem 1.2 at each block of an orthogonal central decomposition of
1 gives Theorem 1.2 for M, for any class P of functionals closed under
positive real scaling.
theorem
Orthogonalization.Blocks.orthAt_one_of_blocks
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
{κ : Type u_2}
[Fintype κ]
(z : κ → H →L[ℂ] H)
(hz : ∀ (j : κ), IsCentralProj M (z j))
(hzo : ∀ (j k : κ), j ≠ k → z j * z k = 0)
(hzs : ∑ j : κ, z j = 1)
(ι : Type u_3)
[Fintype ι]
(h : ∀ (j : κ), OrthAt M (z j) ι)
:
OrthAt M 1 ι
Gluing for arbitrary positive functionals.