OAI/Topology/CoarseAssembly/MultiplierOrthogonalEmbeddings.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoarseAssembly.operatorConjugation_orthogonal line 17
2. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryUnitary_eq_raw line 33
3. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_orthogonalEmbeddings line 42

   Source documentation

   The complementary target summand carries the identity; the two supported boundary classes therefore add in the actual Roe K₁ group.

   theorem multiplierBoundaryClass_orthogonalEmbeddings
       (V : E →ₗᵢ[ℂ] Module X H) (W : F →ₗᵢ[ℂ] Module X H)
       (hVW : V.toContinuousLinearMap.adjoint.comp W.toContinuousLinearMap = 0)
       (A : E →L[ℂ] E) (B : F →L[ℂ] F) (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
       (T L R : multiplierAlgebra (X := X) (H := H))
   …

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