BergSeam.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Finite Berg towers: connectedness and seam formulas

The finite assembled tower is an actual connected unitary when its initial row extension and terminal coefficient are connected. Its layer sum includes the terminal coefficient explicitly. The exact boundary formula gives the seam estimate while accounting for the terminal corner.

lemma OAI.WeakPureInfiniteness.bergTransfer_add line 21
lemma OAI.WeakPureInfiniteness.bergTransfer_sum line 27
lemma OAI.WeakPureInfiniteness.bergFiniteTower_eq_sum line 35
Source documentation
The complete layer sum, including its last transfer corner.
```
lemma bergFiniteTower_eq_sum (s t : I → E) (v : unitary E) (N : ℕ) (x : E) :
    bergFiniteTower s t v N x =
      (∑ k ∈ Finset.range N,
        finiteCuntzTransferIter s t k (bergBottomCoefficient s t v)) +
      finiteCuntzTransferIter s t N x := by
…
```
Mentions: OAI.WeakPureInfiniteness.bergFiniteTower, OAI.WeakPureInfiniteness.finiteCuntzTransferIter, OAI.WeakPureInfiniteness.bergBottomCoefficient

def OAI.WeakPureInfiniteness.bergFiniteTowerUnitary line 50

Source documentation

The bundled unitary represented by a finite tower.

def bergFiniteTowerUnitary (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)
    (v : unitary E) (hv : ∀ i, (v : E) * s i = t i)
    (N : ℕ) (x : unitary E) : unitary E :=
…

lemma OAI.WeakPureInfiniteness.bergFiniteTowerUnitary_continuous line 58
lemma OAI.WeakPureInfiniteness.bergFiniteTowerUnitary_step_one line 65

lemma OAI.WeakPureInfiniteness.bergFiniteTowerUnitary_joined line 76

Source documentation

Connectedness is preserved by the finite tower, rather than assumed for its assembled output.

lemma bergFiniteTowerUnitary_joined (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)
    (v : unitary E) (hv : ∀ i, (v : E) * s i = t i)
    (hvpath : Joined (1 : unitary E) v) (N : ℕ)
    (x : unitary E) (hxpath : Joined (1 : unitary E) x) :
    Joined (1 : unitary E) (bergFiniteTowerUnitary s t hs ht v hv N x) := by
…

Mentions: OAI.WeakPureInfiniteness.bergFiniteTowerUnitary

lemma OAI.WeakPureInfiniteness.bergFiniteTower_succ_right line 91
lemma OAI.WeakPureInfiniteness.bergFiniteTower_boundary line 106
Source documentation
All the variation between adjacent tower heights comes from the terminal coefficient, whose norm is not presumed small.
```
lemma bergFiniteTower_boundary (s t : I → E) (v : unitary E) (N : ℕ) (x : E) :
    bergFiniteTower s t v N x - bergFiniteTower s t v (N + 1) x =
      finiteCuntzTransferIter s t N
        (x - (bergBottomCoefficient s t v + finiteCuntzTransfer s t x)) := by
…
```
Mentions: OAI.WeakPureInfiniteness.bergFiniteTower, OAI.WeakPureInfiniteness.finiteCuntzTransferIter, OAI.WeakPureInfiniteness.bergBottomCoefficient, OAI.WeakPureInfiniteness.finiteCuntzTransfer
lemma OAI.WeakPureInfiniteness.bergFiniteTower_exact_seam line 113

lemma OAI.WeakPureInfiniteness.bergOrthogonal_add_norm_le line 127

Source documentation

Orthogonal source and range supports remove the cost of summing blocks.

lemma bergOrthogonal_add_norm_le (x y : E) (C : ℝ) (hC : 0 ≤ C)
    (hxy : star x * y = 0) (hyx : x * star y = 0)
    (hx : ‖x‖ ≤ C) (hy : ‖y‖ ≤ C) : ‖x + y‖ ≤ C := by
…

lemma OAI.WeakPureInfiniteness.bergOrthogonal_sum_norm_le line 151
lemma OAI.WeakPureInfiniteness.bergSupported_mul_zero line 176
lemma OAI.WeakPureInfiniteness.bergRotationDeviation_support line 184
def OAI.WeakPureInfiniteness.bergFiniteRotation line 203
Source documentation
The sum of rotations in orthogonal corners is a single unitary.
```
def bergFiniteRotation (a : J → E) (S : Finset J) (θ : J → ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.bergFiniteRotation_mem line 207

lemma OAI.WeakPureInfiniteness.bergFiniteRotation_sub_norm_le line 248

Source documentation

Adjacent angle changes in orthogonal blocks are controlled by their largest change, independently of the number of blocks.

lemma bergFiniteRotation_sub_norm_le (a : J → E) (S : Finset J) (θ φ : J → ℝ)
    (ha : ∀ j ∈ S, a j * star (a j) * a j = a j)
    (haa : ∀ j ∈ S, a j * a j = 0)
    (horth : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → bergSupport (a i) * bergSupport (a j) = 0)
    (δ : ℝ) (hδ : 0 ≤ δ) (hangle : ∀ j ∈ S, |θ j - φ j| ≤ δ) :
    ‖bergFiniteRotation a S θ - bergFiniteRotation a S φ‖ ≤ 2 * δ := by
…

Mentions: OAI.WeakPureInfiniteness.bergSupport, OAI.WeakPureInfiniteness.bergFiniteRotation