Sandwich.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The operator-norm sandwich estimate

The norm estimate and closure step do not require an amplified constant-fiber projection to be locally compact. Membership of the approximating sandwiches in the closed algebra is explicit.

theorem OAI.CoarseAssembly.sandwich_error_bound line 24

Source documentation

The uniform 2 ‖Q-P‖ ‖T‖ bound for sandwiching by contractions.

theorem sandwich_error_bound (P Q T : A) (hP : ‖P‖ ≤ 1) (hQ : ‖Q‖ ≤ 1) :
    ‖Q * T * Q - P * T * P‖ ≤ 2 * ‖Q - P‖ * ‖T‖ := by
…

theorem OAI.CoarseAssembly.sandwich_mem_of_tendsto line 50
Source documentation
Norm convergence of the finite-propagation projections passes their sandwiches into any norm-closed algebra. The hypothesis concerns the sandwiches themselves, as required for local compactness in the paper.
```
theorem sandwich_mem_of_tendsto (S : Set A) (hS : IsClosed S) (P : A)
    (Pn : ℕ → A) (hlim : Filter.Tendsto Pn Filter.atTop (nhds P)) (T : A)
    (hmem : ∀ n, Pn n * T * Pn n ∈ S) : P * T * P ∈ S := by
…
```