Roe.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Discrete reduced Roe algebras

Operators act on the actual Hilbert sum ℓ²(X; H). Matrix entries are continuous linear maps on the coefficient Hilbert space. The Roe algebra is the norm-closed star algebra generated by finite-propagation operators whose entries, and adjoint entries, are compact. On a discrete space with finite metric balls these are the usual locally compact generators.

The coefficient space is a parameter; the ample module used in the paper is obtained by taking it to be an infinite-dimensional separable Hilbert space. No compactness is imposed on the averaging projection itself.

theorem OAI.CoarseAssembly.DiscreteRoe.insert_apply line 35
theorem OAI.CoarseAssembly.DiscreteRoe.coordinate_apply line 38
theorem OAI.CoarseAssembly.DiscreteRoe.entry_apply line 40
theorem OAI.CoarseAssembly.DiscreteRoe.entry_continuous line 43
theorem OAI.CoarseAssembly.DiscreteRoe.entry_zero line 47
theorem OAI.CoarseAssembly.DiscreteRoe.entry_add line 51
theorem OAI.CoarseAssembly.DiscreteRoe.entry_smul line 56
theorem OAI.CoarseAssembly.DiscreteRoe.algebra_isClosed line 67
theorem OAI.CoarseAssembly.DiscreteRoe.generator_mem line 70
instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 75) line 75
theorem OAI.CoarseAssembly.DiscreteRoe.map_mem line 83
Source documentation
A continuous spatial homomorphism maps the whole Roe algebra once its range has been proved on the locally compact finite-propagation generators. The range proof remains an obligation, rather than part of the definition.
```
theorem map_mem (φ : Operator X H →⋆ₙₐ[ℂ] Operator Y H) (hφ : Continuous φ)
    (hgen : ∀ T, Generator T → φ T ∈ algebra (X := Y) (H := H))
…
```
Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.Generator, OAI.CoarseAssembly.DiscreteRoe.algebra
theorem OAI.CoarseAssembly.DiscreteRoe.sandwich_mem line 93
Source documentation
The final norm-closure step in the finite-fiber transfer argument.
```
theorem sandwich_mem {P A : Operator X H} {Pn : ℕ → Operator X H}
    (hlim : Filter.Tendsto Pn Filter.atTop (nhds P))
    (hgen : ∀ n, Generator (Pn n * A * Pn n)) : P * A * P ∈ algebra (X := X) (H := H) :=
…
```
Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.Generator, OAI.CoarseAssembly.DiscreteRoe.algebra