OAI/Probability/SKBarriers/Gaussian/SmoothObservables.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.HasExpGrowth.const line 33
  2. theorem OAI.SK.Analytic.HasExpGrowth.finsetSum line 37
  3. theorem OAI.SK.Analytic.HasExpGrowth.fderiv_mul line 47
  4. theorem OAI.SK.Analytic.HasExpGrowth.fderiv_sum line 58
  5. def OAI.SK.Analytic.gradientSquareSum line 68
  6. theorem OAI.SK.Analytic.gradientSquareSum_regular line 72
  7. theorem OAI.SK.Analytic.TranslationInvariant.gradientSquareSum line 87
  8. theorem OAI.SK.Analytic.hierarchyGaussian_shared_stein line 101
  9. theorem OAI.SK.Analytic.hierarchyGaussian_gradientSquare_stein line 127