OAI/Probability/SKBarriers/Calculus/ParameterGrowth.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.ParamExpGrowth line 14
  2. def OAI.SK.Analytic.ParamLinearGrowth line 19
  3. theorem OAI.SK.Analytic.ParamExpGrowth.of_norm_le line 24
  4. theorem OAI.SK.Analytic.ParamExpGrowth.of_bounded line 38
  5. theorem OAI.SK.Analytic.ParamExpGrowth.add line 45
  6. theorem OAI.SK.Analytic.ParamExpGrowth.mul line 59
  7. theorem OAI.SK.Analytic.ParamExpGrowth.norm line 72
  8. theorem OAI.SK.Analytic.ParamLinearGrowth.exp_mul line 78
  9. theorem OAI.SK.Analytic.ParamLinearGrowth.expGrowth line 92
  10. theorem OAI.SK.Analytic.ParamExpGrowth.locallyDominated line 101
  11. theorem OAI.SK.Analytic.ParamExpGrowth.clm line 122
  12. theorem OAI.SK.Analytic.ParamExpGrowth.smul line 125
  13. theorem OAI.SK.Analytic.ParamExpGrowth.gaussian_integral line 132