RoeCalculus.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Finite-propagation matrix calculus

The local-compactness step of the finite-fiber transfer states that sandwiching a locally compact, finite-propagation operator by arbitrary finite-propagation operators preserves local compactness. The multipliers themselves are not assumed locally compact.

theorem OAI.CoarseAssembly.DiscreteRoe.insert_adjoint line 21
theorem OAI.CoarseAssembly.DiscreteRoe.coordinate_adjoint line 27
theorem OAI.CoarseAssembly.DiscreteRoe.entry_star line 30
theorem OAI.CoarseAssembly.DiscreteRoe.vector_eq_sum line 36
theorem OAI.CoarseAssembly.DiscreteRoe.entry_mul_of_finite_column line 50
Source documentation
Matrix multiplication is a finite sum whenever the right-hand column has finite support. This avoids any exchange of infinite sums.
```
theorem entry_mul_of_finite_column (T S : Operator X H) (x y : X) (s : Finset X)
    (hs : ∀ z, z ∉ s → entry S z y = 0) :
    entry (T * S) x y = ∑ z ∈ s, entry T x z * entry S z y := by
…
```
Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.entry
theorem OAI.CoarseAssembly.DiscreteRoe.PropagationLE.star line 66
theorem OAI.CoarseAssembly.DiscreteRoe.column_support line 74
theorem OAI.CoarseAssembly.DiscreteRoe.PropagationLE.mul line 82
theorem OAI.CoarseAssembly.DiscreteRoe.compact_sum line 98
theorem OAI.CoarseAssembly.DiscreteRoe.CompactEntries.mul_left line 105
theorem OAI.CoarseAssembly.DiscreteRoe.CompactEntries.mul_right line 116
theorem OAI.CoarseAssembly.DiscreteRoe.generator_sandwich line 129
Source documentation
Finite-propagation multipliers preserve locally compact generators. In particular this applies to amplified finite-propagation projections, without asserting that those projections are locally compact.
```
theorem generator_sandwich {A Q : Operator X H} {q : ℝ}
    (hA : Generator A) (hq : 0 ≤ q) (hQ : PropagationLE q Q) :
    Generator (Q * A * Q) := by
…
```
Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.Generator, OAI.CoarseAssembly.DiscreteRoe.PropagationLE