TransferCriterion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-fiber Roe transfer criterion

This proves the operator statement of Proposition 5.1. The required finite-propagation scalar contractions between fibers are amplified here; the bounded lift, compactness and compression are constructed, not assumed. The concrete graph family still has to supply these fiber contractions and the averaging approximants.

def OAI.CoarseAssembly.ControlledFiberMaps line 31

Source documentation

Uniform controlled scalar maps preserving the normalized constants.

def ControlledFiberMaps (Q : D → Type*) [∀ u, Fintype (Q u)]
    [∀ u, DecidableEq (Q u)] [PseudoMetricSpace (Sigma Q)] : Prop :=
…

theorem OAI.CoarseAssembly.lift_generator_from_fiber_maps line 39
theorem OAI.CoarseAssembly.finite_fiber_transfer line 81
Source documentation
The finite-fiber transfer lands in the ordinary locally compact reduced Roe algebra. The approximation is an operator-norm approximation of the amplified projection; the projection itself need not be locally compact.
```
theorem finite_fiber_transfer (hD : UniformFiniteBalls D)
    (hX : ∀ x : Sigma Q, ∀ r : ℝ, (Metric.closedBall x r).Finite)
    (hO : ControlledFiberMaps Q)
    (Pn : ℕ → Operator (Sigma Q) H)
    (hlim : Filter.Tendsto Pn Filter.atTop (nhds (fiberProjection Q)))
    (hprop : ∀ n, ∃ r : ℝ, 0 ≤ r ∧ PropagationLE r (Pn n)) :
    MapsToRoe (fiberEmbedding (H := H) Q) := by
…
```
Mentions: OAI.CoarseAssembly.UniformFiniteBalls, OAI.CoarseAssembly.ControlledFiberMaps, OAI.CoarseAssembly.fiberProjection, OAI.CoarseAssembly.fiberEmbedding