RescaledTomitaGraph.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Rescaled Tomita graphs in a fixed two-coordinate Hilbert space

A fixed conjugation identifies the conjugate copy of the Hilbert space with the original one. In these coordinates the graph vector is (x Ω, c J (x* Ω)). The same identification is used for both algebras. No closability or modular spectral theorem is needed for the closed linear graph subspace or the elementary projection comparison below.

abbrev OAI.KadisonKastler.TomitaGraphHilbert line 26
Source documentation
The fixed Hilbert space in which the two rescaled graphs are compared.
```
abbrev TomitaGraphHilbert (H : Type*) := Generator.FiniteHilbert (Fin 2) H
```
Mentions: OAI.Generator.FiniteHilbert
def OAI.KadisonKastler.rescaledGraphVector line 29
Source documentation
Graph coordinates after identifying the conjugate Hilbert space by J.
```
def rescaledGraphVector (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (x : H →L[ℂ] H) : TomitaGraphHilbert H :=
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert
theorem OAI.KadisonKastler.rescaledGraphVector_zero line 33
theorem OAI.KadisonKastler.rescaledGraphVector_one line 36
def OAI.KadisonKastler.rescaledGraphMap line 41
Source documentation
The conjugation in the second coordinate makes the graph map complex-linear rather than conjugate-linear.
```
def rescaledGraphMap (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (c : ℝ) : Algebra P →ₗ[ℂ] TomitaGraphHilbert H where
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.TomitaGraphHilbert
theorem OAI.KadisonKastler.rescaledGraphMap_apply line 56

theorem OAI.KadisonKastler.norm_rescaledGraphVector_sq line 61

Source documentation

The defining weighted graph norm, with no restriction on the scale.

theorem norm_rescaledGraphVector_sq (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (x : H →L[ℂ] H) :
    ‖rescaledGraphVector J Ω c x‖ ^ 2 = ‖x Ω‖ ^ 2 + c ^ 2 * ‖star x Ω‖ ^ 2 := by
…

Mentions: OAI.KadisonKastler.rescaledGraphVector

def OAI.KadisonKastler.rescaledGraphSubspace line 69
Source documentation
The closed linear rescaled graph.
```
def rescaledGraphSubspace (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (c : ℝ) : Submodule ℂ (TomitaGraphHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert
instance OAI.KadisonKastler.rescaledGraphSubspace_complete line 73
theorem OAI.KadisonKastler.rescaledGraphVector_mem line 78

def OAI.KadisonKastler.rescaledGraphProjection line 84

Source documentation

Orthogonal projection onto the closed graph.

def rescaledGraphProjection (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (c : ℝ) : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H :=
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert

theorem OAI.KadisonKastler.rescaledGraphProjection_vector line 88

theorem OAI.KadisonKastler.rescaledGraph_bound_on_closure line 96

Source documentation

A bound on the defining graph vectors extends to their actual closure.

theorem rescaledGraph_bound_on_closure
    (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) (B : ℝ)
    (hB : ∀ x : Algebra P,
      ‖T (rescaledGraphVector J Ω c x.val)‖ ≤ B * ‖rescaledGraphVector J Ω c x.val‖)
    {ξ : TomitaGraphHilbert H} (hξ : ξ ∈ rescaledGraphSubspace P J Ω c) :
    ‖T ξ‖ ≤ B * ‖ξ‖ := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.rescaledGraphSubspace

theorem OAI.KadisonKastler.norm_comp_rescaledGraphProjection_le line 108

Source documentation

A graph-vector estimate bounds the operator after graph projection.

theorem norm_comp_rescaledGraphProjection_le
    (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) {B : ℝ} (hB : 0 ≤ B)
    (hv : ∀ x : Algebra P,
      ‖T (rescaledGraphVector J Ω c x.val)‖ ≤ B * ‖rescaledGraphVector J Ω c x.val‖) :
    ‖T * rescaledGraphProjection P J Ω c‖ ≤ B := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.rescaledGraphProjection

theorem OAI.KadisonKastler.norm_product_reverse_of_selfAdjoint line 122

theorem OAI.KadisonKastler.norm_rescaledGraphProjection_sub_le line 131

Source documentation

Two directional graph-vector estimates give a uniform comparison of the actual orthogonal graph projections.

theorem norm_rescaledGraphProjection_sub_le
    (P Q : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    {B : ℝ} (hB : 0 ≤ B)
    (hPQ : ∀ x : Algebra P,
      ‖(1 - rescaledGraphProjection Q J Ω c) (rescaledGraphVector J Ω c x.val)‖ ≤
        B * ‖rescaledGraphVector J Ω c x.val‖)
    (hQP : ∀ x : Algebra Q,
      ‖(1 - rescaledGraphProjection P J Ω c) (rescaledGraphVector J Ω c x.val)‖ ≤
        B * ‖rescaledGraphVector J Ω c x.val‖) :
    ‖rescaledGraphProjection P J Ω c - rescaledGraphProjection Q J Ω c‖ ≤ 2 * B := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphProjection, OAI.KadisonKastler.rescaledGraphVector