RoeTransfer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Norm-closure and spatial factorization for the finite-fiber transfer

The missing construction of the finite-propagation lift is isolated as an explicit witness here; it is not treated as a published input. Once a lift has been constructed by matchings, the following argument proves that the spatial homomorphism lands in the actual reduced Roe algebra.

theorem OAI.CoarseAssembly.DiscreteRoe.conjugation_continuous line 26

theorem OAI.CoarseAssembly.DiscreteRoe.conjugation_mem_of_sandwich_lifts line 33

Source documentation

The range proof after constructing the matching lift of each generator.

theorem conjugation_mem_of_sandwich_lifts
    (finiteBalls : ∀ x : X, ∀ r : ℝ, (Metric.closedBall x r).Finite)
    (V : Module D H →ₗᵢ[ℂ] Module X H)
    (P : Operator X H) (Pn : ℕ → Operator X H)
    (hlim : Filter.Tendsto Pn Filter.atTop (nhds P))
    (hprop : ∀ n, ∃ r : ℝ, 0 ≤ r ∧ PropagationLE r (Pn n))
    (hlift : ∀ T : Operator D H, Generator T →
      ∃ A : Operator X H, Generator A ∧ P * A * P = operatorConjugation V T)
    {T : Operator D H} (hT : T ∈ algebra (X := D) (H := H)) :
…

Mentions: OAI.CoarseAssembly.DiscreteRoe.Module, OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.PropagationLE, OAI.CoarseAssembly.DiscreteRoe.Generator, OAI.CoarseAssembly.operatorConjugation, OAI.CoarseAssembly.DiscreteRoe.algebra

theorem OAI.CoarseAssembly.DiscreteRoe.conjugationHom_apply line 53
theorem OAI.CoarseAssembly.DiscreteRoe.conjugationHom_injective line 58
theorem OAI.CoarseAssembly.DiscreteRoe.conjugationHom_comp_apply line 68
Source documentation
Exact operator factorization remains exact after restriction to Roe algebras. This is the final operator identity Ad V ∘ Ad E = Ad I.
```
theorem conjugationHom_comp_apply
    (E : Module B H →ₗᵢ[ℂ] Module D H)
    (V : Module D H →ₗᵢ[ℂ] Module X H)
    (hE : MapsToRoe E) (hV : MapsToRoe V) (hVE : MapsToRoe (V.comp E))
    (T : algebra (X := B) (H := H)) :
…
```
Mentions: OAI.CoarseAssembly.DiscreteRoe.Module, OAI.CoarseAssembly.DiscreteRoe.MapsToRoe, OAI.CoarseAssembly.DiscreteRoe.algebra