ConnectedCocycleGluing.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Connected gluing of the actual finite cocycle paths

The paths for all finite cocycle coefficients use one partition. This lets the weighted sum be deformed continuously to one, with both Gram defects controlled throughout the deformation. The cyclic seam is retained exactly.

lemma OAI.WeakPureInfiniteness.glued_product_commutator line 19

lemma OAI.WeakPureInfiniteness.clock_endomorphism_commutator line 33

Source documentation

Transport a commutator through one step of the actual endomorphism.

lemma clock_endomorphism_commutator (φ : E →⋆ₙₐ[ℂ] E)
    (α : unitary E →* unitary E) (hα : ∀ u, (α u : E) = φ u)
    (u : unitary E) (e f : E) (C η : ℝ)
    (hc : ‖(u : E) * e - e * (u : E)‖ ≤ C)
    (he : ‖φ e - f‖ ≤ η) :
    ‖(α u : E) * f - f * (α u : E)‖ ≤ C + 2 * η := by
…

lemma OAI.WeakPureInfiniteness.clock_iterate_commutator line 57
def OAI.WeakPureInfiniteness.clockTailTime line 76
Source documentation
Move from a chosen sampling time to the terminal time.
```
def clockTailTime (a t : unitInterval) : unitInterval :=
…
```
lemma OAI.WeakPureInfiniteness.clockTailTime_continuous line 82
lemma OAI.WeakPureInfiniteness.clockTailTime_zero line 87
lemma OAI.WeakPureInfiniteness.clockTailTime_one line 92

def OAI.WeakPureInfiniteness.clockCoefficientContraction line 98

Source documentation

Coefficient contraction using the two paths on the same partition.

def clockCoefficientContraction (α : unitary E →* unitary E) (hα : Continuous α)
    {u v : unitary E} (p : Path u 1) (q : Path v 1) (a : unitInterval) (j : ℕ) :
    Path (u * (α^[j]) (q a)) 1 where
…

lemma OAI.WeakPureInfiniteness.clockCoefficientContraction_commutator line 108

lemma OAI.WeakPureInfiniteness.exists_connected_rohlin_polar_tolerance line 127

Source documentation

Small diagonal commutators throughout a coefficient homotopy give a connected polar correction of its initial weighted sum.

lemma exists_connected_rohlin_polar_tolerance [Nontrivial E]
    {I : Type*} [Fintype I] [DecidableEq I] (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (e : I → E),
      (∀ i, IsStarProjection (e i)) → (∑ i, e i) = 1 →
      (∀ i j, i ≠ j → e i * e j = 0) →
      ∀ (v : I → unitInterval → unitary E),
        (∀ i, Continuous (v i)) → (∀ i, v i 1 = 1) →
        (∀ t i, ‖(v i t : E) * e i - e i * (v i t : E)‖ ≤ δ) →
        ∃ u : unitary E, Joined (1 : unitary E) u ∧
          ‖(u : E) - finiteRohlinSum (fun i => v i 0) e‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRohlinSum

lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_clock_step line 190

Source documentation

The mesh estimate keeps the additive modulus error.

lemma finiteCocycleCoefficient_clock_step (α : unitary E →* unitary E) (w : unitary E)
    (hα : ∀ u v : unitary E, ‖(α u : E) - α v‖ ≤ ‖(u : E) - v‖)
    {N : ℕ} (p : Path (finiteGroupCocycle α w N) 1)
    (L ρ : ℝ) (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b| + ρ)
    (k : ℕ) (a b : unitInterval) :
    ‖(w : E) * α (finiteCocycleCoefficient α w p k a) -
      finiteCocycleCoefficient α w p (k + 1) b‖ ≤ L * |(a : ℝ) - b| + ρ := by
…

Mentions: OAI.WeakPureInfiniteness.finiteGroupCocycle, OAI.WeakPureInfiniteness.finiteCocycleCoefficient

def OAI.WeakPureInfiniteness.clockGridPoint line 205
def OAI.WeakPureInfiniteness.clockPeriodicCoefficient line 211
lemma OAI.WeakPureInfiniteness.clockPeriodicCoefficient_zero line 216

lemma OAI.WeakPureInfiniteness.clockPeriodicCoefficient_step line 227

Source documentation

The last-to-first transition uses the exact endpoint equality, including the height-one case.

lemma clockPeriodicCoefficient_step (α : unitary E →* unitary E) (w : unitary E)
    (hα : ∀ u v : unitary E, ‖(α u : E) - α v‖ ≤ ‖(u : E) - v‖)
    {N : ℕ} (hN : 0 < N) (p : Path (finiteGroupCocycle α w N) 1)
    (L ρ : ℝ) (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b| + ρ)
    (k : ZMod N) :
    ‖(w : E) * α (clockPeriodicCoefficient α w hN p k) -
      clockPeriodicCoefficient α w hN p (k + 1)‖ ≤ L / N + ρ := by
…

Mentions: OAI.WeakPureInfiniteness.finiteGroupCocycle, OAI.WeakPureInfiniteness.clockPeriodicCoefficient

lemma OAI.WeakPureInfiniteness.connected_rohlin_cocycle_of_family line 267

Source documentation

All paths on the same partition give a connected approximate coboundary. The finite tolerance can be chosen after the height.

lemma connected_rohlin_cocycle_of_family [Nontrivial E]
    {N : ℕ} [NeZero N] (hN : 0 < N) (φ : E →⋆ₙₐ[ℂ] E)
    (α : unitary E →* unitary E) (hco : ∀ u, (α u : E) = φ u)
    (hcont : Continuous α)
    (hα : ∀ u v : unitary E, ‖(α u : E) - α v‖ ≤ ‖(u : E) - v‖)
    (w : unitary E) (e : ZMod N → E)
    (he : ∀ k, IsStarProjection (e k))
    (heo : ∀ k l, k ≠ l → e k * e l = 0)
    (L ρ C η ε δ : ℝ) (hL : 0 ≤ L) (hρ : 0 ≤ ρ)
    (hs : ∀ k, ‖φ (e k) - e (k + 1)‖ ≤ η)
    (r : ∀ n : ℕ, n ≤ N → Path (finiteGroupCocycle α w n) 1)
    (hr : ∀ n hn, ClockPathControl (r n hn) e L ρ C)
…

Mentions: OAI.WeakPureInfiniteness.finiteGroupCocycle, OAI.WeakPureInfiniteness.ClockPathControl

lemma OAI.WeakPureInfiniteness.exists_joint_connected_coboundary_at_height line 331

Source documentation

All partition, path, and Gram hypotheses are discharged for the actual commuting full binary rows. Only the displayed mesh term remains.

lemma exists_joint_connected_coboundary_at_height [Nontrivial E]
    (s t : Fin 2 → 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)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hcomm : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ‖(binaryRowUnitary s t hs ht hsum htsum : E) * finiteRowShift s u - u‖ ≤
        (320 * Real.pi) * Real.sqrt (2 ^ m : ℕ) / (2 ^ m : ℕ) + ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.binaryRowUnitary, OAI.WeakPureInfiniteness.finiteRowShift

lemma OAI.WeakPureInfiniteness.exists_connected_binary_row_conjugacy line 386

Source documentation

The finite-height mesh term tends to zero, with every other tolerance chosen only after the height. This is a genuine connected conjugacy result for two commuting full binary Cuntz rows.

lemma exists_connected_binary_row_conjugacy [Nontrivial E]
    (s t : Fin 2 → 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)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hcomm : bergRowsCommute s t) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ∀ i, ‖(u : E) * s i * star (u : E) - t i‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute