OAI/Probability/SKSupport/Foundations/SoftAbs.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.boundedSmooth_of_polynomial_deriv line 18
  2. lemma OAI.ZeroTemperatureSK.Heat.contDiff_tanh line 41
  3. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_tanh line 46
  4. lemma OAI.ZeroTemperatureSK.Heat.boundedSmooth_tanh_mul line 54
  5. def OAI.ZeroTemperatureSK.Heat.softAbs line 69
  6. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_softAbs line 71
  7. lemma OAI.ZeroTemperatureSK.Heat.regularDatum_softAbs line 80
  8. lemma OAI.ZeroTemperatureSK.Heat.softAbs_lipschitz line 88
  9. lemma OAI.ZeroTemperatureSK.Heat.softAbs_even line 95
  10. lemma OAI.ZeroTemperatureSK.Heat.exp_abs_bounds line 99
  11. lemma OAI.ZeroTemperatureSK.Heat.softAbs_bounds line 112
  12. lemma OAI.ZeroTemperatureSK.Heat.semigroup_add line 137
  13. lemma OAI.ZeroTemperatureSK.Heat.logSemigroup_add line 147
  14. lemma OAI.ZeroTemperatureSK.Heat.logSemigroup_terminal_domination line 163
  15. lemma OAI.ZeroTemperatureSK.Heat.logSemigroup_terminal_stability line 194