OAI/Topology/CoarseAssembly/EmbeddingBoundaryComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equality of Roe boundary classes from two embeddings of one operator

  1. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryUnitary_embedding line 19
  2. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_embedding line 36

    Source documentation

    Two embeddings of the same operator give the same class whenever their transition is a Roe multiplier. Coefficient embeddings satisfy this via propagation zero.

    theorem multiplierBoundaryClass_embedding
    (V W : E →ₗᵢ[ℂ] Module X H) (S : E →L[ℂ] E) (hS : IsSelfAdjoint S)
    (F G : multiplierAlgebra (X := X) (H := H)) (hF : IsSelfAdjoint F) (hG : IsSelfAdjoint G)
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.Module, OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra