OAI/Analysis/KadisonKastler/GaussianStateAnalytic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Entire coefficients of the concrete Gaussian operator average

  1. theorem OAI.KadisonKastler.gaussianStateAverage_vector_differentiable line 18
  2. theorem OAI.KadisonKastler.gaussianStateAverage_coefficient_differentiable line 27