OAI/Probability/SKSupport/Foundations/ExponentialBoundLipschitz.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_of_lipschitz line 18
  2. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_exp line 30
  3. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.bdd_mul line 43
  4. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_weightExp line 51
  5. lemma OAI.ZeroTemperatureSK.Heat.deriv_weightExp line 59
  6. lemma OAI.ZeroTemperatureSK.Heat.exp_iteratedDeriv_weight line 64
  7. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_exp_iteratedDeriv line 74
  8. lemma OAI.ZeroTemperatureSK.Heat.hasDerivWithinAt_varianceHeat_exp line 82
  9. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_scaled_space line 98
  10. lemma OAI.ZeroTemperatureSK.Heat.deriv_varianceHeat line 127
  11. lemma OAI.ZeroTemperatureSK.Heat.deriv_deriv_varianceHeat line 132
  12. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_equation line 139
  13. lemma OAI.ZeroTemperatureSK.Heat.logarithmic_heat_equation line 151
  14. def OAI.ZeroTemperatureSK.Heat.varianceLogHeat line 177
  15. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_eq_logSemigroup line 180
  16. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_exp_pos line 189
  17. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_equation line 196