CornerContractionPath.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Controlled cancellation paths in a fixed corner

A relative unitary compressed into one range cancels its adjoint compressed into an orthogonal equivalent range by an explicit quarter-turn. The path has an angular Lipschitz bound independent of that unitary. Its complement is retained throughout; this does not construct a fixed approximately central corner for a growing family of cocycles.

def OAI.WeakPureInfiniteness.cornerCompression line 22
Source documentation
Extend a unitary in the initial corner of a by the identity elsewhere.
```
def cornerCompression (a z : E) : E := a * z * star a + (1 - a * star a)
```
lemma OAI.WeakPureInfiniteness.cornerCompression_star line 24
lemma OAI.WeakPureInfiniteness.cornerCompression_mul line 29
lemma OAI.WeakPureInfiniteness.cornerCompression_unit line 60
lemma OAI.WeakPureInfiniteness.cornerCompression_mem line 66
lemma OAI.WeakPureInfiniteness.cornerCompression_conjugate line 79
lemma OAI.WeakPureInfiniteness.cornerCompression_neg line 84
def OAI.WeakPureInfiniteness.cornerCancellationPath line 89
Source documentation
The cancellation uses the rotation from the first range to the second.
```
def cornerCancellationPath (a b z : E) (θ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.cornerRotation_relations line 93
lemma OAI.WeakPureInfiniteness.cornerRotation_quarter_mul_second line 119
lemma OAI.WeakPureInfiniteness.cornerCancellationPath_zero line 141
lemma OAI.WeakPureInfiniteness.cornerCancellationPath_continuous line 145
lemma OAI.WeakPureInfiniteness.cornerCancellationPath_mem line 151
lemma OAI.WeakPureInfiniteness.cornerCancellationPath_quarter line 169
lemma OAI.WeakPureInfiniteness.cornerCancellationPath_sub_norm_le line 194

lemma OAI.WeakPureInfiniteness.exists_controlled_cornerCancellation_path line 230

Source documentation

An actual unitary path with fixed angular cost, including both endpoints.

lemma exists_controlled_cornerCancellation_path (q a b z : E) (hqstar : star q = q)
    (haa : star a * a = q) (hbb : star b * b = q) (hab : star a * b = 0)
    (haq : a * q = a) (hbq : b * q = b)
    (hqz : q * z = z) (hzq : z * q = z)
    (hzz : star z * z = q) (hzz' : z * star z = q) :
    ∃ u : ℝ → unitary E, Continuous u ∧
      (u 0 : E) = cornerCompression a z * cornerCompression b (star z) ∧
      (u (Real.pi / 2) : E) = 1 ∧
      ∀ θ φ, ‖(u θ : E) - u φ‖ ≤ 4 * |θ - φ| := by
…

Mentions: OAI.WeakPureInfiniteness.cornerCompression