OAI/Probability/SKSupport/Foundations/Const.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.RegularDatum.const line 18
  2. lemma OAI.ZeroTemperatureSK.Heat.boundedSmooth_semigroup line 22
  3. lemma OAI.ZeroTemperatureSK.Heat.regularDatum_semigroup line 31
  4. lemma OAI.ZeroTemperatureSK.Heat.regularDatum_logSemigroup line 44
  5. lemma OAI.ZeroTemperatureSK.Heat.integrable_mul_standardGaussianPDF line 67
  6. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_standardGaussianPDF line 77
  7. lemma OAI.ZeroTemperatureSK.Heat.standardGaussian_stein line 90
  8. def OAI.ZeroTemperatureSK.Heat.ExponentialBound line 121
  9. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.of_bounded line 124
  10. lemma OAI.ZeroTemperatureSK.Heat.integrable_abs_mul_exp_abs line 128
  11. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_scaled line 139
  12. lemma OAI.ZeroTemperatureSK.Heat.integrable_scaled_of_expBound line 150
  13. lemma OAI.ZeroTemperatureSK.Heat.integrable_mul_scaled_of_expBound line 161
  14. def OAI.ZeroTemperatureSK.Heat.scaled line 177
  15. lemma OAI.ZeroTemperatureSK.Heat.semigroup_eq_scaled line 180
  16. lemma OAI.ZeroTemperatureSK.Heat.continuous_scaled line 193
  17. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_scaled line 213