UniformGraphComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform comparison of the two rescaled graph projections

Directional bounds proved at scales at least one extend to every positive scale by the reciprocal graph symmetry. The two directions then bound the norm of the difference of orthogonal projections.

theorem OAI.KadisonKastler.graph_directional_vector_le_of_norm line 21

Source documentation

The norm of a directional projection product bounds all defining graph vectors in that direction.

theorem graph_directional_vector_le_of_norm
    (M N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c B : ℝ)
    (hbound : ‖(1 - rescaledGraphProjection N J Ω c) * rescaledGraphProjection M J Ω c‖ ≤ B)
    (x : Algebra M) :
    ‖(1 - rescaledGraphProjection N J Ω c) (rescaledGraphVector J Ω c x.val)‖ ≤
      B * ‖rescaledGraphVector J Ω c x.val‖ := by
…

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

theorem OAI.KadisonKastler.graph_directional_all_positive line 36

Source documentation

A large-scale directional bound controls every positive scale.

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

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

theorem OAI.KadisonKastler.uniform_rescaledGraphProjection_comparison line 52

Source documentation

Two large-scale directional estimates give a uniform norm estimate for the actual closed graph projections at every positive scale.

theorem uniform_rescaledGraphProjection_comparison
    (M N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (Ω : H) {B : ℝ} (hB : 0 ≤ B)
    (hMN : ∀ c : ℝ, 1 ≤ c →
      ‖(1 - rescaledGraphProjection N J Ω c) * rescaledGraphProjection M J Ω c‖ ≤ B)
    (hNM : ∀ c : ℝ, 1 ≤ c →
      ‖(1 - rescaledGraphProjection M J Ω c) * rescaledGraphProjection N J Ω c‖ ≤ B)
    {c : ℝ} (hc : 0 < c) :
    ‖rescaledGraphProjection M J Ω c - rescaledGraphProjection N J Ω c‖ ≤ 2 * B :=
…

Mentions: OAI.KadisonKastler.rescaledGraphProjection