OAI/Analysis/OInfinity/HalfFlipRecursion.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Finite recursive intertwiners for the O∞ half-flip

For two finite Cuntz families, the transfer operator sends x to ∑ i, t i * x * star (s i). Its Cesàro means are contractions and satisfy a uniform recursive intertwining estimate. These means are not asserted to be unitary; constructing nearby connected unitaries remains a separate step.

  1. def OAI.WeakPureInfiniteness.finiteCuntzTransfer line 21

    Source documentation

    The finite transfer operator from the family s to the family t.

    def finiteCuntzTransfer (s t : I → E) (x : E) : E :=
…
  2. lemma OAI.WeakPureInfiniteness.finiteCuntzDiagonal_mul_term line 25
  3. def OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom line 40

    Source documentation

    The diagonal corner sum is a genuine star homomorphism.

    def finiteCuntzDiagonalHom (s : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) : E →⋆ₙₐ[ℂ] E where
…
  4. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_mul line 52
  5. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_star_mul line 62
  6. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_continuous line 82
  7. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_sub line 88
  8. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_norm_le line 93
  9. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_sub_norm_le line 103
  10. def OAI.WeakPureInfiniteness.finiteCuntzTransferIter line 111

    Source documentation

    Iteration is kept explicit to expose the last boundary term.

    def finiteCuntzTransferIter (s t : I → E) : ℕ → E → E
  | 0, x => x
  | n + 1, x => finiteCuntzTransfer s t (finiteCuntzTransferIter s t n x)

omit [DecidableEq I] in

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer

  11. lemma OAI.WeakPureInfiniteness.finiteCuntzTransferIter_zero line 116
  12. lemma OAI.WeakPureInfiniteness.finiteCuntzTransferIter_succ line 120
  13. lemma OAI.WeakPureInfiniteness.finiteCuntzTransferIter_norm_le line 124
  14. def OAI.WeakPureInfiniteness.finiteCuntzTransferSum line 132
  15. lemma OAI.WeakPureInfiniteness.finiteCuntzTransferSum_succ line 136
  16. lemma OAI.WeakPureInfiniteness.finiteCuntzTransferSum_intertwining line 142

    Source documentation

    The entire intertwining error is the difference of two boundary terms.

    lemma finiteCuntzTransferSum_intertwining (s t : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (x : E) (i : I) :
    finiteCuntzTransferSum s t n x * s i - t i * finiteCuntzTransferSum s t n x =
      x * s i - t i * finiteCuntzTransferIter s t n x := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransferSum, OAI.WeakPureInfiniteness.finiteCuntzTransferIter

  17. def OAI.WeakPureInfiniteness.finiteCuntzCesaro line 160

    Source documentation

    Cesàro smoothing of the recursive intertwiner.

    def finiteCuntzCesaro (s t : I → E) (n : ℕ) (x : E) : E :=
…
  18. lemma OAI.WeakPureInfiniteness.finiteCuntzCesaro_intertwining line 163
  19. lemma OAI.WeakPureInfiniteness.finiteCuntzCesaro_norm_le line 171
  20. lemma OAI.WeakPureInfiniteness.finiteCuntzCesaro_intertwining_norm_le line 185
  21. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_mul_annihilator line 208

    Source documentation

    The transfer operator annihilates the unused source corner.

    lemma finiteCuntzTransfer_mul_annihilator (s t : I → E) (x q : E)
    (hq : ∀ i, star (s i) * q = 0) : finiteCuntzTransfer s t x * q = 0 := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer

  22. lemma OAI.WeakPureInfiniteness.finiteCuntzTransferSum_mul_annihilator line 213
  23. lemma OAI.WeakPureInfiniteness.finiteCuntzCesaro_mul_annihilator line 224

    Source documentation

    In the unused source corner, smoothing retains only the scaled seed. This exposes the boundary obstruction to a unitary normalization.

    lemma finiteCuntzCesaro_mul_annihilator (s t : I → E) (n : ℕ) (x q : E)
    (hq : ∀ i, star (s i) * q = 0) :
    finiteCuntzCesaro s t n x * q = ((n : ℝ) + 1)⁻¹ • (x * q) := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzCesaro

  24. lemma OAI.WeakPureInfiniteness.finiteCuntzCesaro_dist_unitary_lower line 232

    Source documentation

    A seed-one Cesàro mean stays far from every unitary when a nonzero unused source corner survives. It is not a unitary half-flip witness.

    lemma finiteCuntzCesaro_dist_unitary_lower (s t : I → E) (n : ℕ) (q : E)
    (hq : ∀ i, star (s i) * q = 0) (hq0 : q ≠ 0) (u : unitary E) :
    1 - ((n : ℝ) + 1)⁻¹ ≤ ‖(u : E) - finiteCuntzCesaro s t n 1‖ := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzCesaro

  25. lemma OAI.WeakPureInfiniteness.unitary_conjugation_error_eq line 255

    Source documentation

    Unitary conjugation has exactly the same error as recursive intertwining.

    lemma unitary_conjugation_error_eq (u : unitary E) (a b : E) :
    ‖(u : E) * a * star (u : E) - b‖ = ‖(u : E) * a - b * (u : E)‖ := by
…
  26. lemma OAI.WeakPureInfiniteness.unitary_conjugation_error_le line 268

    Source documentation

    A later unitary completion must control its distance from the recursive intertwiner; the error cost of that replacement is at most twice the distance.

    lemma unitary_conjugation_error_le (u : unitary E) (x a b : E)
    (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) :
    ‖(u : E) * a * star (u : E) - b‖ ≤ 2 * ‖(u : E) - x‖ + ‖x * a - b * x‖ := by
…
  27. def OAI.WeakPureInfiniteness.partialIsometrySwap line 286

    Source documentation

    Swap the orthogonal initial and final spaces of a square-zero partial isometry, and act identically on their common complement.

    def partialIsometrySwap (a : E) : E :=
…
  28. def OAI.WeakPureInfiniteness.partialIsometryCompletion line 291

    Source documentation

    The chosen two-swap completion, with fixed initial support p and spare isometry r. This is a polynomial in the partial intertwiner v.

    def partialIsometryCompletion (r p v : E) : E :=
…
  29. lemma OAI.WeakPureInfiniteness.partialIsometryCompletion_continuous line 294
  30. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_sub line 299
  31. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_sub_norm_le line 305
  32. lemma OAI.WeakPureInfiniteness.partialIsometryCompletion_sub_norm_le line 315

    Source documentation

    On a fixed pair of support projections, the completion is 2-Lipschitz. The fixed right swap is unitary, so it contributes no norm loss.

    lemma partialIsometryCompletion_sub_norm_le [Nontrivial E] (r p v w : E)
    (hr : star r * r = 1) (hu : partialIsometrySwap (r * p) ∈ unitary E)
    (hi : star v * v = star w * w) (hf : v * star v = w * star w) :
    ‖partialIsometryCompletion r p v - partialIsometryCompletion r p w‖ ≤
      2 * ‖v - w‖ := by
…

    Mentions: OAI.WeakPureInfiniteness.partialIsometrySwap, OAI.WeakPureInfiniteness.partialIsometryCompletion

  33. lemma OAI.WeakPureInfiniteness.norm_add_star_of_square_zero line 347
  34. lemma OAI.WeakPureInfiniteness.partialIsometryCompletion_sub_norm_le_one line 368

    Source documentation

    With the common spare range orthogonal to both final supports, the completion is actually nonexpansive: its varying part is an off-diagonal selfadjoint corner, whose norm equals the norm of that corner.

    lemma partialIsometryCompletion_sub_norm_le_one [Nontrivial E] (r p v w : E)
    (hr : star r * r = 1) (hu : partialIsometrySwap (r * p) ∈ unitary E)
    (hi : star v * v = star w * w) (hf : v * star v = w * star w)
    (hvr : star r * v = 0) (hwr : star r * w = 0) :
    ‖partialIsometryCompletion r p v - partialIsometryCompletion r p w‖ ≤
      ‖v - w‖ := by
…

    Mentions: OAI.WeakPureInfiniteness.partialIsometrySwap, OAI.WeakPureInfiniteness.partialIsometryCompletion

  35. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_star line 403
  36. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_sq line 408
  37. def OAI.WeakPureInfiniteness.partialIsometrySwapUnitary line 423
  38. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_mul_initial line 428
  39. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_isometry_projection_mem line 444
  40. lemma OAI.WeakPureInfiniteness.selfadjoint_unitary_joined_one line 460

    Source documentation

    A selfadjoint unitary belongs to the identity path component. The two short paths run through its scalar rotation by I.

    lemma selfadjoint_unitary_joined_one [Nontrivial E] (u : unitary E)
    (hu : star (u : E) = (u : E)) : Joined (1 : unitary E) u := by
…
  41. lemma OAI.WeakPureInfiniteness.partialIsometrySwapUnitary_joined line 488
  42. lemma OAI.WeakPureInfiniteness.exists_explicit_connected_unitary_extension line 495

    Source documentation

    One isometry in the common complement completes a partial isometry to a unitary in the identity component. This does not assert recursive invariance.

    lemma exists_explicit_connected_unitary_extension [Nontrivial E] (v r : E)
    (hv : v * star v * v = v) (hr : star r * r = 1)
    (hpr : (star v * v) * r = 0) (hqr : (v * star v) * r = 0) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (u : E) = partialIsometryCompletion r (star v * v) v ∧
      (u : E) * (star v * v) = v := by
…

    Mentions: OAI.WeakPureInfiniteness.partialIsometryCompletion

  43. lemma OAI.WeakPureInfiniteness.exists_connected_unitary_extension line 572

    Source documentation

    Forgetting the explicit formula recovers the usual extension statement.

    lemma exists_connected_unitary_extension [Nontrivial E] (v r : E)
    (hv : v * star v * v = v) (hr : star r * r = 1)
    (hpr : (star v * v) * r = 0) (hqr : (v * star v) * r = 0) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧ (u : E) * (star v * v) = v := by
…
  44. lemma OAI.WeakPureInfiniteness.exists_continuous_connected_unitary_extensions line 582

    Source documentation

    A continuous family of partial intertwiners with fixed initial support has a continuous family of connected unitary extensions given by the same polynomial formula. No local choice of unitaries is needed.

    lemma exists_continuous_connected_unitary_extensions {X : Type*} [TopologicalSpace X]
    [Nontrivial E] (v : X → E) (r p : E) (hvcont : Continuous v)
    (hv : ∀ x, v x * star (v x) * v x = v x)
    (hp : ∀ x, star (v x) * v x = p) (hr : star r * r = 1)
    (hpr : p * r = 0) (hqr : ∀ x, (v x * star (v x)) * r = 0) :
    ∃ u : X → unitary E, Continuous u ∧ ∀ x,
      Joined (1 : unitary E) (u x) ∧
      (u x : E) = partialIsometryCompletion r p (v x) ∧ (u x : E) * p = v x := by
…

    Mentions: OAI.WeakPureInfiniteness.partialIsometryCompletion

  45. lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_star line 606
  46. lemma OAI.WeakPureInfiniteness.exists_connected_transfer_step line 612

    Source documentation

    Complete one recursive step to an actual connected unitary. The right hand side retains the previous unitary w; it is not a conjugacy assertion.

    lemma exists_connected_transfer_step [Nontrivial E] (s t : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (r : E) (hr : star r * r = 1)
    (hsr : ∀ i, star (s i) * r = 0) (htr : ∀ i, star (t i) * r = 0)
    (w : unitary E) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ∀ i, (u : E) * s i = t i * (w : E) := by
…
  47. lemma OAI.WeakPureInfiniteness.exists_continuous_connected_transfer_steps line 661

    Source documentation

    Completing each transfer in a continuous family yields a continuous family of connected unitaries. The completion does not increase the norm variation of the preceding unitaries. This applies in particular to any path of preceding unitaries, without claiming a fixed point.

    lemma exists_continuous_connected_transfer_steps {X : Type*} [TopologicalSpace X]
    [Nontrivial E] (s t : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (r : E) (hr : star r * r = 1)
    (hsr : ∀ i, star (s i) * r = 0) (htr : ∀ i, star (t i) * r = 0)
    (w : X → unitary E) (hw : Continuous w) :
    ∃ u : X → unitary E, Continuous u ∧
      (∀ x, Joined (1 : unitary E) (u x) ∧
        ∀ i, (u x : E) * s i = t i * (w x : E)) ∧
      ∀ x y, ‖(u x : E) - u y‖ ≤ ‖(w x : E) - w y‖ := by
…
  48. lemma OAI.WeakPureInfiniteness.exists_continuous_transfer_path_tower line 737

    Source documentation

    Iterating the continuous completion produces a tower of unitary paths. Adjacent paths match at their endpoints, and adjacent levels satisfy exact recursive intertwining. The estimate controls each finite part of the tower; it does not assert that consecutive levels become close.

    lemma exists_continuous_transfer_path_tower [Nontrivial E] (s t : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (r : E) (hr : star r * r = 1)
    (hsr : ∀ i, star (s i) * r = 0) (htr : ∀ i, star (t i) * r = 0) :
    ∃ u : ℕ → unitInterval → unitary E,
      (∀ n, Continuous (u n)) ∧ u 0 0 = 1 ∧
      (∀ n, u n 1 = u (n + 1) 0) ∧
      (∀ n x i, (u (n + 1) x : E) * s i = t i * (u n x : E)) ∧
      ∀ n x y, ‖(u n x : E) - u n y‖ ≤ ‖(u 0 x : E) - u 0 y‖ := by
…
  49. lemma OAI.WeakPureInfiniteness.exists_connected_infinite_transfer_step line 772

    Source documentation

    For the two tensor-factor Cuntz families, one unused product isometry lies in the common complement of the first N ranges.

    lemma exists_connected_infinite_transfer_step [Nontrivial E] (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hc : ∀ i j, Commute (star (t i)) (s j)) (N : ℕ) (w : unitary E) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ∀ i < N, (u : E) * s i = t i * (w : E) := by
…