OAI/Analysis/OInfinity/BergShift.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite Berg smoothing along a Cuntz corner shift

A finite family of orthogonal corner rotations can have a large angle in the middle and zero angles at both ends. The commutator with a row generator is controlled by adjacent angle differences. The unitary and connectedness assertions are proved for the finite construction. Matching a terminal corner between the two different tensor-factor rows is still a separate obligation.

  1. def OAI.WeakPureInfiniteness.bergCornerLift line 22

    Source documentation

    Adjoin the complementary identity to a nonunital corner map.

    def bergCornerLift (φ : E →⋆ₙₐ[ℂ] E) (x : E) : E := 1 - φ 1 + φ x
  2. lemma OAI.WeakPureInfiniteness.bergCornerMap_real_smul line 24
  3. lemma OAI.WeakPureInfiniteness.bergCornerMap_rotation_deviation line 28
  4. lemma OAI.WeakPureInfiniteness.bergCornerLift_finiteRotation line 39
  5. def OAI.WeakPureInfiniteness.bergShiftAngles line 48

    Source documentation

    Angles shifted by one layer, with a zero at the new bottom.

    def bergShiftAngles (θ : ℕ → ℝ) : ℕ → ℝ
  | 0 => 0
  | k + 1 => θ k
  6. lemma OAI.WeakPureInfiniteness.bergShiftAngles_zero line 52
  7. lemma OAI.WeakPureInfiniteness.bergShiftAngles_succ line 53
  8. lemma OAI.WeakPureInfiniteness.bergFiniteRotation_pad_zero line 56
  9. lemma OAI.WeakPureInfiniteness.bergCornerLift_shift line 63
  10. lemma OAI.WeakPureInfiniteness.bergFiniteRotation_shift_norm_le line 72

    Source documentation

    Vanishing endpoint angles leave only adjacent angular changes at the seam.

    lemma bergFiniteRotation_shift_norm_le (φ : E →⋆ₙₐ[ℂ] E) (a : ℕ → E)
    (hshift : ∀ k, φ (a k) = a (k + 1)) (θ : ℕ → ℝ) (N : ℕ)
    (ha : ∀ k < N + 2, a k * star (a k) * a k = a k)
    (haa : ∀ k < N + 2, a k * a k = 0)
    (horth : ∀ i < N + 2, ∀ j < N + 2, i ≠ j →
      bergSupport (a i) * bergSupport (a j) = 0)
    (hzero : θ 0 = 0) (hend : θ (N + 1) = 0)
    (δ : ℝ) (hδ : 0 ≤ δ) (hstep : ∀ k ≤ N, |θ (k + 1) - θ k| ≤ δ) :
    ‖bergFiniteRotation a (Finset.range (N + 1)) θ -
      bergCornerLift φ (bergFiniteRotation a (Finset.range (N + 1)) θ)‖ ≤ 2 * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergFiniteRotation, OAI.WeakPureInfiniteness.bergCornerLift

  11. lemma OAI.WeakPureInfiniteness.bergFiniteRotation_joined line 97

    Source documentation

    Every finite orthogonal rotation lies in the identity component.

    lemma bergFiniteRotation_joined {J : Type*} (a : J → E) (S : Finset J) (θ : J → ℝ)
    (ha : ∀ j ∈ S, a j * star (a j) * a j = a j)
    (haa : ∀ j ∈ S, a j * a j = 0)
    (horth : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → bergSupport (a i) * bergSupport (a j) = 0) :
    Joined (1 : unitary E)
      ⟨bergFiniteRotation a S θ, bergFiniteRotation_mem a S θ ha haa horth⟩ := by
…

    Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergFiniteRotation, OAI.WeakPureInfiniteness.bergFiniteRotation_mem

  12. def OAI.WeakPureInfiniteness.bergCornerIterHom line 125

    Source documentation

    Iteration as an actual nonunital star homomorphism.

    def bergCornerIterHom (φ : E →⋆ₙₐ[ℂ] E) : ℕ → E →⋆ₙₐ[ℂ] E
  | 0 => NonUnitalStarAlgHom.id ℂ E
  | n + 1 => φ.comp (bergCornerIterHom φ n)
  13. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_zero line 129
  14. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_succ line 132
  15. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_layer_zero line 135
  16. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_support line 141
  17. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_partial line 145
  18. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_square_zero line 151
  19. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_orthogonal line 157

    Source documentation

    A rotation supported in the bottom layer has disjoint iterated corners.

    lemma bergCornerIterHom_orthogonal (φ : E →⋆ₙₐ[ℂ] E) (a : E)
    (hsupport : bergSupport a * bergTowerLayer φ 0 = bergSupport a)
    {n m : ℕ} (hne : n ≠ m) :
    bergSupport (bergCornerIterHom φ n a) * bergSupport (bergCornerIterHom φ m a) = 0 := by
…

    Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.bergCornerIterHom

  20. lemma OAI.WeakPureInfiniteness.bergSupport_mul_star line 177
  21. lemma OAI.WeakPureInfiniteness.bergFiniteRotation_quarter_mul_initial line 192

    Source documentation

    At a quarter-turn peak, the assembled finite rotation transports the specified initial corner exactly. Other tower levels do not affect it.

    lemma bergFiniteRotation_quarter_mul_initial {J : Type*} (a : J → E) (S : Finset J)
    (θ : J → ℝ) (j : J) (hj : j ∈ S) (hθj : θ j = Real.pi / 2)
    (ha : ∀ k ∈ S, a k * star (a k) * a k = a k)
    (haa : ∀ k ∈ S, a k * a k = 0)
    (horth : ∀ k ∈ S, ∀ l ∈ S, k ≠ l → bergSupport (a k) * bergSupport (a l) = 0) :
    bergFiniteRotation a S θ * (star (a j) * a j) = a j := by
…

    Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergFiniteRotation

  22. lemma OAI.WeakPureInfiniteness.bergCornerLift_mul_generator line 224
  23. lemma OAI.WeakPureInfiniteness.bergFiniteRotation_commutator_norm_le line 231
  24. lemma OAI.WeakPureInfiniteness.bergIteratedRotation_commutator_norm_le line 256

    Source documentation

    The canonical iterates of a bottom-supported corner satisfy the finite Berg commutator estimate for every generator in the row.

    lemma bergIteratedRotation_commutator_norm_le (s : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsnorm : ∀ i, ‖s i‖ ≤ 1) (a : E)
    (ha : a * star a * a = a) (haa : a * a = 0)
    (hsupport : bergSupport a * bergTowerLayer (finiteCuntzDiagonalHom s hs) 0 = bergSupport a)
    (θ : ℕ → ℝ) (N : ℕ) (hzero : θ 0 = 0) (hend : θ (N + 1) = 0)
    (δ : ℝ) (hδ : 0 ≤ δ) (hstep : ∀ k ≤ N, |θ (k + 1) - θ k| ≤ δ) (i : I) :
    let b := fun k => bergCornerIterHom (finiteCuntzDiagonalHom s hs) k a
…

    Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom, OAI.WeakPureInfiniteness.bergCornerIterHom

  25. lemma OAI.WeakPureInfiniteness.exists_connected_berg_rotation line 280

    Source documentation

    A smoothed finite tower transports its peak corner by an actual connected unitary and nearly commutes with every row generator.

    lemma exists_connected_berg_rotation (s : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsnorm : ∀ i, ‖s i‖ ≤ 1) (a : E)
    (ha : a * star a * a = a) (haa : a * a = 0)
    (hsupport : bergSupport a * bergTowerLayer (finiteCuntzDiagonalHom s hs) 0 = bergSupport a)
    (θ : ℕ → ℝ) (N K : ℕ) (hK : K < N + 1) (hpeak : θ K = Real.pi / 2)
    (hzero : θ 0 = 0) (hend : θ (N + 1) = 0)
    (δ : ℝ) (hδ : 0 ≤ δ) (hstep : ∀ k ≤ N, |θ (k + 1) - θ k| ≤ δ) :
    let b := fun k => bergCornerIterHom (finiteCuntzDiagonalHom s hs) k a
…

    Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom, OAI.WeakPureInfiniteness.bergCornerIterHom