GraphReciprocal.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal rescaling of closed Tomita graphs

Conjugating and interchanging the two coordinates sends the graph at c to the graph at 1/c. This norm-preserving real-linear map transfers the directional estimates to small positive scales.

def OAI.KadisonKastler.graphFlipValue line 19
theorem OAI.KadisonKastler.graphFlipValue_norm line 23
theorem OAI.KadisonKastler.conjugation_real_smul line 32
def OAI.KadisonKastler.graphReciprocalFlip line 39
Source documentation
The reciprocal graph symmetry, viewed as a real-linear isometry.
```
def graphReciprocalFlip (J : H ≃ₗᵢ⋆[ℂ] H) :
    TomitaGraphHilbert H →L[ℝ] TomitaGraphHilbert H :=
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert
theorem OAI.KadisonKastler.graphReciprocalFlip_norm line 56

theorem OAI.KadisonKastler.graphReciprocalFlip_vector line 61

Source documentation

Exact reciprocal graph formula on the defining algebra vectors.

theorem graphReciprocalFlip_vector (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (Ω : H) {c : ℝ} (hc : c ≠ 0) (x : H →L[ℂ] H) :
    graphReciprocalFlip J (rescaledGraphVector J Ω c x) =
      c • rescaledGraphVector J Ω c⁻¹ (star x) := by
…

Mentions: OAI.KadisonKastler.graphReciprocalFlip, OAI.KadisonKastler.rescaledGraphVector

theorem OAI.KadisonKastler.graphReciprocalFlip_mem line 75

Source documentation

The reciprocal symmetry maps the entire closed graph to the reciprocal closed graph, by continuity.

theorem graphReciprocalFlip_mem (P : VonNeumannAlgebra H)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H)
    {c : ℝ} (hc : c ≠ 0) {ξ : TomitaGraphHilbert H}
    (hξ : ξ ∈ rescaledGraphSubspace P J Ω c) :
    graphReciprocalFlip J ξ ∈ rescaledGraphSubspace P J Ω c⁻¹ := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphSubspace, OAI.KadisonKastler.graphReciprocalFlip

theorem OAI.KadisonKastler.norm_sub_projection_le line 91
theorem OAI.KadisonKastler.graph_distance_le line 98

theorem OAI.KadisonKastler.graph_directional_reciprocal line 107

Source documentation

A directional vector bound at the reciprocal scale gives the same bound at the original positive scale.

theorem graph_directional_reciprocal
    (M N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (Ω : H) {c : ℝ} (hc : 0 < c) {B : ℝ}
    (hbound : ∀ x : Algebra M,
      ‖(1 - rescaledGraphProjection N J Ω c⁻¹) (rescaledGraphVector J Ω c⁻¹ x.val)‖ ≤
        B * ‖rescaledGraphVector J Ω c⁻¹ x.val‖)
    (x : Algebra M) :
    ‖(1 - rescaledGraphProjection N J Ω c) (rescaledGraphVector J Ω c x.val)‖ ≤
      B * ‖rescaledGraphVector J Ω c x.val‖ := by
…

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