OAI/Topology/CoarseAssembly/PointwiseEmbeddingTransition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Pointwise coefficient transitions have propagation zero

  1. theorem OAI.CoarseAssembly.DiscreteRoe.blockIsometry_adjoint_apply line 18
  2. theorem OAI.CoarseAssembly.DiscreteRoe.pointwiseEmbeddingTransition_apply line 26
  3. theorem OAI.CoarseAssembly.DiscreteRoe.pointwiseEmbeddingTransition_propagation line 33
  4. theorem OAI.CoarseAssembly.DiscreteRoe.pointwiseEmbeddingTransition_multiplier line 41
  5. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_pointwiseEmbedding line 48

    Source documentation

    Choice of pointwise embeddings does not change the actual Roe boundary class.

    theorem multiplierBoundaryClass_pointwiseEmbedding
    (finiteBalls : ∀ x : X, ∀ r : ℝ, (Metric.closedBall x r).Finite)
    (V W : ∀ x, E x →ₗᵢ[ℂ] H) (S : lp E 2 →L[ℂ] lp E 2) (hS : IsSelfAdjoint S)
    (F G : multiplierAlgebra (X := X) (H := H)) (hF : IsSelfAdjoint F) (hG : IsSelfAdjoint G)
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra