OAI/Topology/CoarseAssembly/TensorFibers.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Amplifying finite-fiber operators

The algebraic Hilbert tensor product of a finite scalar fiber with the coefficient Hilbert space is isometrically the fiber's vector-valued ℓ² space. This gives the norm-controlled amplification used in each transfer block, using Mathlib's Hilbert tensor-product operator norm theorem.

  1. def OAI.CoarseAssembly.fiberTensorBilinear line 23
  2. def OAI.CoarseAssembly.fiberTensorMap line 42
  3. theorem OAI.CoarseAssembly.fiberTensorMap_tmul_apply line 45
  4. theorem OAI.CoarseAssembly.fiberTensorMap_inner line 48
  5. def OAI.CoarseAssembly.fiberTensorIsometry line 65
  6. theorem OAI.CoarseAssembly.fiberTensorMap_surjective line 76
  7. def OAI.CoarseAssembly.fiberTensorEquiv line 84
  8. theorem OAI.CoarseAssembly.fiberTensorEquiv_apply line 88
  9. theorem OAI.CoarseAssembly.fiberTensor_single line 91
  10. theorem OAI.CoarseAssembly.fiberTensor_constant line 97
  11. def OAI.CoarseAssembly.amplifyFiber line 105
  12. theorem OAI.CoarseAssembly.amplifyFiber_norm_le line 111
  13. theorem OAI.CoarseAssembly.amplifyFiber_tensor line 124
  14. theorem OAI.CoarseAssembly.amplifyFiber_single line 132
  15. theorem OAI.CoarseAssembly.amplifyFiber_constant line 138