FixedSpareStabilization.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Sampled-path stabilization in a fixed spare corner

A cyclic permutation converts a diagonal of path samples into adjacent increments. The finite matrix corner and its complement remain explicit.

lemma OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary_one line 23
lemma OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary_star line 33
lemma OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary_sub_norm_le line 46
lemma OAI.WeakPureInfiniteness.fixedSparePermutation_conjugate_diagonal line 57

lemma OAI.WeakPureInfiniteness.fixedSpareDiagonal_commutator line 75

Source documentation

Exact diagonal entries of the stabilized commutator.

lemma fixedSpareDiagonal_commutator (σ : Equiv.Perm I)
    (x y : I → unitary E) (hx : ∀ i, Commute q (x i : E))
    (hy : ∀ i, Commute q (y i : E)) :
    let d := fixedSpareDiagonalUnitary q r hqstar hqq hr x hx
…

Mentions: OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary

lemma OAI.WeakPureInfiniteness.exists_fixedSpareDiagonal_path line 103

Source documentation

Every increment of size at most one gives a 9π path after finite cyclic stabilization. This estimate is independent of the number of samples.

lemma exists_fixedSpareDiagonal_path [Nontrivial E] (N : ℕ) [NeZero N]
    (q : E) (r : ZMod N → E) (hqstar : star q = q) (hqq : q * q = q)
    (hr : ∀ i j, star (r i) * r j = if i = j then q else 0)
    (x y : ZMod N → unitary E) (hx : ∀ i, Commute q (x i : E))
    (hy : ∀ i, Commute q (y i : E))
    (hstep : ∀ i, ‖(y i : E) * ((x i : E) * star (x (i - 1) : E)) - 1‖ ≤ 1) :
    ∃ p : Path (1 : unitary E) (fixedSpareDiagonalUnitary q r hqstar hqq hr y hy),
      ∀ a b, ‖(p a : E) - p b‖ ≤ (9 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary

def OAI.WeakPureInfiniteness.fixedSpareProjection line 139
Source documentation
Complement of the fixed isometry's range.
```
def fixedSpareProjection (z : E) : E := 1 - z * star z
```
lemma OAI.WeakPureInfiniteness.fixedSpareProjection_star line 141
lemma OAI.WeakPureInfiniteness.fixedSpareProjection_sq line 145
lemma OAI.WeakPureInfiniteness.fixedSpareProjection_mul line 154
lemma OAI.WeakPureInfiniteness.fixedSpareUnitary_support line 159
def OAI.WeakPureInfiniteness.fixedSpareCopies line 183
Source documentation
The zeroth copy is the original corner; all other copies lie inside its fixed complement. No equality between the total range and one is used.
```
def fixedSpareCopies (z : E) (s : I → E) (i₀ i : I) : E :=
…
```
lemma OAI.WeakPureInfiniteness.fixedSpareCopies_gram line 187
lemma OAI.WeakPureInfiniteness.fixedSpareCopies_diagonal line 230
def OAI.WeakPureInfiniteness.fixedSpareMesh line 257
Source documentation
Equal mesh on a cyclic index set, with its last point strictly below one.
```
def fixedSpareMesh (N : ℕ) [NeZero N] (i : ZMod N) : unitInterval :=
…
```
lemma OAI.WeakPureInfiniteness.fixedSpareMesh_zero line 264
lemma OAI.WeakPureInfiniteness.fixedSpareMesh_step line 269
lemma OAI.WeakPureInfiniteness.fixedSpareMesh_last line 280
lemma OAI.WeakPureInfiniteness.fixedSpare_mul_star_sub_one_norm line 290

lemma OAI.WeakPureInfiniteness.exists_uniform_fixedSpare_path line 298

Source documentation

A connected unitary that fixes one isometry has a uniformly controlled path, using actual finite spare copies and actual samples of the given path.

lemma exists_uniform_fixedSpare_path [Nontrivial E]
    (s : ℕ → E) (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (z : E) (hz : star z * z = 1) (u : unitary E)
    (p : Path (1 : unitary E) u) (hfix : ∀ t, (p t : E) * z = z)
    (L : ℝ) (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b|) :
    ∃ v : Path (1 : unitary E) u,
      ∀ a b, ‖(v a : E) - v b‖ ≤ (9 * Real.pi) * |(a : ℝ) - b| := by
…