OAI/Analysis/OperatorAlgebra/GaussianConvolutionApproximation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual integrable L² Gaussian convolution kernels give a uniformly contractive strong approximate identity on vector-valued L².

  1. lemma OAI.WeakPureInfiniteness.realGaussianDensity_continuous line 15
  2. lemma OAI.WeakPureInfiniteness.realGaussianDensity_bound line 19
  3. def OAI.WeakPureInfiniteness.gaussianConvolutionKernel line 23
  4. lemma OAI.WeakPureInfiniteness.gaussianConvolutionKernel_continuous line 26
  5. lemma OAI.WeakPureInfiniteness.gaussianConvolutionKernel_integrable line 30
  6. lemma OAI.WeakPureInfiniteness.gaussianConvolutionKernel_bound line 35
  7. lemma OAI.WeakPureInfiniteness.gaussianConvolutionKernel_memLp line 44
  8. def OAI.WeakPureInfiniteness.gaussianConvolutionVector line 55
  9. lemma OAI.WeakPureInfiniteness.gaussianConvolutionVector_ae line 58
  10. lemma OAI.WeakPureInfiniteness.gaussianConvolutionVector_integrable line 61
  11. lemma OAI.WeakPureInfiniteness.gaussianConvolutionKernel_apply line 68
  12. lemma OAI.WeakPureInfiniteness.gaussianConvolutionVector_apply line 96
  13. lemma OAI.WeakPureInfiniteness.gaussianConvolutionVector_strong line 105