OAI/Analysis/KadisonKastler/GaussianOperatorContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Norm continuity of Gaussian-smeared operator orbits

The uniform derivative bound upgrades the existing vectorwise analytic construction to operator norm continuity. This is the smoothing step needed to integrate an invariant, possibly nonnormal, state.

  1. theorem OAI.KadisonKastler.gaussianDerivativeEnvelope_nonneg line 23
  2. theorem OAI.KadisonKastler.gaussianStateAverage_norm_sub_le line 28
  3. theorem OAI.KadisonKastler.gaussianStateAverage_continuous line 57