BandProducts.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact band products and the actual adjacent-depth corner

Products sample their first coefficient at the shifted index. The final lemma uses the concrete Cuntz relation at neighboring depths, with its inner-letter orthogonality condition. It is local in the tower cell; no cyclic boundary cell is silently identified with the next depth.

lemma OAI.WeakPureInfiniteness.towerBand_star line 22

lemma OAI.WeakPureInfiniteness.towerBand_mul line 40

Source documentation

The first coefficient is evaluated at τ i, rather than i.

lemma towerBand_mul (e : I → E) (σ τ : Equiv.Perm I) (x y : I → E)
    (hee : ∀ i, e i * e i = e i)
    (ho : ∀ i j, i ≠ j → e i * e j = 0) :
    towerBand e σ x * towerBand e τ y =
      towerBand e (σ * τ) (fun i => x (τ i) * e (τ i) * y i) := by
…

Mentions: OAI.WeakPureInfiniteness.towerBand

lemma OAI.WeakPureInfiniteness.towerBand_mul_norm_le line 67

Source documentation

The product estimate applies to the actual shifted coefficient.

lemma towerBand_mul_norm_le (e : I → E) (σ τ : Equiv.Perm I) (x y : I → E)
    (he : ∀ i, IsStarProjection (e i))
    (ho : ∀ i j, i ≠ j → e i * e j = 0)
    (M : ℝ) (hM : 0 ≤ M)
    (hxy : ∀ i, ‖x (τ i) * e (τ i) * y i‖ ≤ M) :
    ‖towerBand e σ x * towerBand e τ y‖ ≤ M := by
…

Mentions: OAI.WeakPureInfiniteness.towerBand

lemma OAI.WeakPureInfiniteness.towerBand_norm_le_of_sandwich line 77

Source documentation

It suffices to bound the actual corner of each coefficient.

lemma towerBand_norm_le_of_sandwich (e : I → E) (σ : Equiv.Perm I) (x : I → E)
    (he : ∀ i, IsStarProjection (e i))
    (ho : ∀ i j, i ≠ j → e i * e j = 0)
    (M : ℝ) (hM : 0 ≤ M)
    (hx : ∀ i, ‖e (σ i) * x i * e i‖ ≤ M) :
    ‖towerBand e σ x‖ ≤ M := by
…

Mentions: OAI.WeakPureInfiniteness.towerBand

lemma OAI.WeakPureInfiniteness.mixed_corner_norm_le line 95
lemma OAI.WeakPureInfiniteness.binaryBand_row_norm line 116

lemma OAI.WeakPureInfiniteness.binaryRowIterate_mixed_corner_bound line 128

Source documentation

The overlap of the two actual neighboring-depth bands is small when r ≠ l. The depth n+1 is literal, including at a tower boundary.

lemma binaryRowIterate_mixed_corner_bound {N : ℕ} (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (e : ZMod N → E) (he : ∀ j, IsStarProjection (e j))
    (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η)
    (n : ℕ) (i r l : Fin 2) (hrl : r ≠ l) (j : ZMod N) :
    ‖star (finiteRowShiftIterate s n (s i * s r)) * e (j + 1) *
        finiteRowShiftIterate s (n + 1) (s l) * e j‖ ≤
      (2 * (n : ℝ) + 3) * η := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.finiteRowShiftIterate