BandOperators.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Dimension-independent estimates for finite tower bands

A fixed band has orthogonal initial and final projection corners. Its norm is therefore bounded by its largest coefficient, independently of the number of tower cells. This is the estimate used for adjacent path samples.

lemma OAI.WeakPureInfiniteness.orthogonalSelfAdjoint_sum_bound line 21

lemma OAI.WeakPureInfiniteness.orthogonalSupported_sum_norm_le line 43

Source documentation

A family with pairwise orthogonal initial and final supports has the supremum norm estimate; in particular no cardinality factor is needed.

lemma orthogonalSupported_sum_norm_le (b : I → E)
    (hl : ∀ i j, i ≠ j → star (b i) * b j = 0)
    (hr : ∀ i j, i ≠ j → b i * star (b j) = 0)
    (M : ℝ) (hM : 0 ≤ M) (hb : ∀ i, ‖b i‖ ≤ M) :
    ‖∑ i, b i‖ ≤ M := by
…

def OAI.WeakPureInfiniteness.towerBand line 69
Source documentation
One finite matrix band, indexed by its domain cells.
```
def towerBand (e : I → E) (σ : Equiv.Perm I) (x : I → E) : E :=
…
```
lemma OAI.WeakPureInfiniteness.towerBand_norm_le line 72

lemma OAI.WeakPureInfiniteness.towerBand_sub_norm_le line 103

Source documentation

Changing every coefficient by at most ε changes a fixed band by at most ε, independently of the number of cells.

lemma towerBand_sub_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)
    (ε : ℝ) (hε : 0 ≤ ε) (hxy : ∀ i, ‖x i - y i‖ ≤ ε) :
    ‖towerBand e σ x - towerBand e σ y‖ ≤ ε := by
…

Mentions: OAI.WeakPureInfiniteness.towerBand