CentralIsometries.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Global approximately central isometries

An unused Cuntz isometry supplies the bottom of a strictly contracting recursion. Its norm limit is an actual isometry. The damping gives estimates on the whole algebra, including the last tail; no tail norm is discarded.

def OAI.WeakPureInfiniteness.centralDampedBase line 20
def OAI.WeakPureInfiniteness.centralDampedStep line 23
lemma OAI.WeakPureInfiniteness.centralDampedStep_contracting line 26
def OAI.WeakPureInfiniteness.centralDampedLimit line 37
lemma OAI.WeakPureInfiniteness.centralDampedLimit_eq line 41
lemma OAI.WeakPureInfiniteness.centralDampedBase_star_mul line 47
lemma OAI.WeakPureInfiniteness.centralDampedBase_star_mul_image line 63
lemma OAI.WeakPureInfiniteness.centralDampedImage_star_mul_base line 68

lemma OAI.WeakPureInfiniteness.centralDampedLimit_isometry line 76

Source documentation

The fixed point remains an isometry, by contraction of its multiplicative defect. This also controls the infinite terminal tail.

lemma centralDampedLimit_isometry (φ : E →⋆ₙₐ[ℂ] E) (r : E) (ε : ℝ)
    (ρ : ℝ≥0) (hρ : ρ < 1) (hr : star r * r = 1)
    (hε : ε * ε + (ρ : ℝ) * ρ = 1)
    (horth : ∀ x, star r * φ x = 0) :
    star (centralDampedLimit φ r ε ρ hρ) * centralDampedLimit φ r ε ρ hρ = 1 := by
…

Mentions: OAI.WeakPureInfiniteness.centralDampedLimit

lemma OAI.WeakPureInfiniteness.eq_zero_of_damped_norm line 112

lemma OAI.WeakPureInfiniteness.centralDampedLimit_orthogonal line 121

Source documentation

Orthogonal spare isometries give orthogonal limiting isometries.

lemma centralDampedLimit_orthogonal (φ : E →⋆ₙₐ[ℂ] E) (r b : E) (ε : ℝ)
    (ρ : ℝ≥0) (hρ : ρ < 1) (hrb : star r * b = 0)
    (hr : ∀ x, star r * φ x = 0) (hb : ∀ x, star b * φ x = 0) :
    star (centralDampedLimit φ r ε ρ hρ) * centralDampedLimit φ b ε ρ hρ = 0 := by
…

Mentions: OAI.WeakPureInfiniteness.centralDampedLimit

lemma OAI.WeakPureInfiniteness.centralDampedLimit_commutes line 153
lemma OAI.WeakPureInfiniteness.finiteCuntzDiagonal_orthogonal_unused line 175
lemma OAI.WeakPureInfiniteness.finiteCuntzDiagonal_mul_generator line 184
lemma OAI.WeakPureInfiniteness.finiteCuntzGenerator_star_mul_diagonal line 189
lemma OAI.WeakPureInfiniteness.centralDampedLimit_mul_generator line 195
lemma OAI.WeakPureInfiniteness.centralDampedLimit_generator_star_mul line 208
lemma OAI.WeakPureInfiniteness.centralDampedLimit_commutes_other_row line 220

lemma OAI.WeakPureInfiniteness.centralDampedLimit_commutator_bounds line 253

Source documentation

Global bounds for the actual limiting isometry.

lemma centralDampedLimit_commutator_bounds (s : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (r : E) (hr : star r * r = 1) (hrs : ∀ i, star (s i) * r = 0)
    (ε : ℝ) (hε0 : 0 ≤ ε) (ρ : ℝ≥0) (hρ : ρ < 1)
    (hε : ε * ε + (ρ : ℝ) * ρ = 1) (i : I) :
    let R := centralDampedLimit (finiteCuntzDiagonalHom s hs) r ε ρ hρ
…

Mentions: OAI.WeakPureInfiniteness.centralDampedLimit, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom

lemma OAI.WeakPureInfiniteness.exists_central_damping line 299

lemma OAI.WeakPureInfiniteness.exists_approximately_central_cuntz_row line 321

Source documentation

A whole infinite orthogonal row approximately commutes with the prescribed finite row and exactly commutes with the other tensor factor.

lemma exists_approximately_central_cuntz_row [Nontrivial E] (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hc : ∀ i j, Commute (s i) (t j) ∧ Commute (s i) (star (t j)))
    (n : ℕ) (δ : ℝ) (hδ : 0 < δ) :
    ∃ r : ℕ → E,
      (∀ j k, star (r j) * r k = if j = k then 1 else 0) ∧
      (∀ j i, i < n → ‖r j * s i - s i * r j‖ < δ ∧
        ‖r j * star (s i) - star (s i) * r j‖ < δ) ∧
      ∀ j k, Commute (r j) (t k) ∧ Commute (r j) (star (t k)) := by
…