OAI/Probability/SKSupport/Density/GaussianTails.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.const line 13
  2. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.neg line 16
  3. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.add line 20
  4. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.sub line 35
  5. lemma OAI.ZeroTemperatureSK.Heat.ExponentialBound.pow line 38
  6. lemma OAI.ZeroTemperatureSK.Heat.gaussian_expBound_tendsto_zero line 43
  7. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.regular line 75
  8. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.exponentialBound line 77
  9. lemma OAI.ZeroTemperatureSK.Heat.certW_odd line 81
  10. lemma OAI.ZeroTemperatureSK.Heat.certV_even line 86
  11. lemma OAI.ZeroTemperatureSK.Heat.certZ_even line 89
  12. lemma OAI.ZeroTemperatureSK.Heat.odd_zero line 93
  13. lemma OAI.ZeroTemperatureSK.Heat.cert_flux_continuous line 98
  14. lemma OAI.ZeroTemperatureSK.Heat.certificate_growth line 117