RelativeUnitaryPath.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform paths for relative unitaries

In a fixed corner carrying a coisometric pair, a relative unitary that almost commutes with that pair admits an explicit uniform path bound. The endpoint is extended by the identity on the ambient complement. The existence of such a pair in a prescribed corner is an input, not a consequence asserted here.

def OAI.WeakPureInfiniteness.relativeUnitaryExtension line 21
Source documentation
Extend a relative unitary by the identity on the complementary corner.
```
def relativeUnitaryExtension (q z : E) : E := z + (1 - q)
```
lemma OAI.WeakPureInfiniteness.relativeUnitaryExtension_mem line 23
lemma OAI.WeakPureInfiniteness.relativeUnitaryExtension_decomposition_error line 37
lemma OAI.WeakPureInfiniteness.unitaryPath_mul_sub_norm_le line 62

lemma OAI.WeakPureInfiniteness.exists_uniform_relativeUnitary_path line 82

Source documentation

The fixed-pair hypotheses give a numerical bound independent of the relative unitary. The ambient complement is present in the initial point.

lemma exists_uniform_relativeUnitary_path (q a b z : E)
    (hqstar : star q = q) (hqq : q * q = q)
    (haa : star a * a = q) (hbb : star b * b = q) (hab : star a * b = 0)
    (hsum : a * star a + b * star b = q)
    (hqz : q * z = z) (hzq : z * q = z)
    (hzz : star z * z = q) (hzz' : z * star z = q)
    (δ : ℝ) (hδ : 0 ≤ δ) (hsmall : 4 * δ < 2)
    (haz : ‖z * a - a * z‖ ≤ δ) (hbz : ‖z * b - b * z‖ ≤ δ) :
    ∃ u : unitary E, (u : E) = relativeUnitaryExtension q z ∧
      ∃ p : Path u 1, ∀ t s, ‖(p t : E) - p s‖ ≤ (32 * Real.pi) * |(t : ℝ) - s| := by
…

Mentions: OAI.WeakPureInfiniteness.relativeUnitaryExtension