OAI/Analysis/OperatorAlgebra/KernelIntegralBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Product-integrable bounds and a measure-preserving change of variables for the scalar kernels used in crossed-product reconstruction.

  1. lemma OAI.WeakPureInfiniteness.integrable_weighted_scalar_kernel line 14
  2. lemma OAI.WeakPureInfiniteness.kernelDifference_measurePreserving line 24
  3. lemma OAI.WeakPureInfiniteness.kernel_integral_change_variables line 32
  4. def OAI.WeakPureInfiniteness.scalarKernelMatrixCoefficient line 65
  5. lemma OAI.WeakPureInfiniteness.scalarKernelMatrixCoefficient_continuous line 70
  6. lemma OAI.WeakPureInfiniteness.scalarKernelMatrixCoefficient_bound line 82