OAI/Probability/SKSupport/Density/GaussianDecay.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.linear_abs_le_quadratic line 12
  2. lemma OAI.ZeroTemperatureSK.Heat.integrable_gaussian_linear line 25
  3. lemma OAI.ZeroTemperatureSK.Heat.integrable_gaussian_expBound line 34
  4. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.mul line 45
  5. lemma OAI.ZeroTemperatureSK.Heat.gaussian_convolution_quadratic line 58
  6. lemma OAI.ZeroTemperatureSK.Heat.continuous_dslope_zero line 83
  7. def OAI.ZeroTemperatureSK.Heat.quotientExtension line 90
  8. lemma OAI.ZeroTemperatureSK.Heat.BackwardShape.nonzero line 92
  9. lemma OAI.ZeroTemperatureSK.Heat.BackwardShape.dslope_nonzero line 96
  10. lemma OAI.ZeroTemperatureSK.Heat.quotientExtension_continuous line 102
  11. lemma OAI.ZeroTemperatureSK.Heat.quotientExtension_eq line 106
  12. lemma OAI.ZeroTemperatureSK.Heat.BackwardShape.abs_eq line 112
  13. lemma OAI.ZeroTemperatureSK.Heat.quotient_linear_bound line 119
  14. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_of_linear_bound line 151
  15. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_quotient line 157