OAI/Topology/CoarseAssembly/ProjectionBlocks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Spatial block projections

Adjoints commute with uniformly bounded Hilbert direct sums. Under the explicit flattening equivalence, the sum of constant-fiber projections is exactly the spatial projection V V* used by the Roe transfer.

  1. theorem OAI.CoarseAssembly.blockOperator_adjoint line 25
  2. theorem OAI.CoarseAssembly.blockIsometry_toCLM line 37
  3. theorem OAI.CoarseAssembly.block_constantProjection line 48
  4. theorem OAI.CoarseAssembly.flattenOperator_eq_conjugation line 60
  5. theorem OAI.CoarseAssembly.flatten_constantProjection line 80

    Source documentation

    Equality with the actual spatial projection, not merely agreement on formal constant-fiber symbols.

    theorem flatten_constantProjection :
    flattenOperator (Q := Q) (H := H) (blockOperator (fun i => constantProjection (H := H) (Q i))
…

    Mentions: OAI.CoarseAssembly.flattenOperator, OAI.CoarseAssembly.blockOperator, OAI.CoarseAssembly.constantProjection

  6. theorem OAI.CoarseAssembly.flattenOperator_sub line 89
  7. theorem OAI.CoarseAssembly.flattenOperator_mul line 100
  8. theorem OAI.CoarseAssembly.flattenOperator_tendsto line 108