OAI/Probability/SKValue/Gaussian/DensityJump.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.SmoothTerminal.const line 11
  2. def OAI.SKValue.ForwardDensityData.gaussian line 18
  3. lemma OAI.SKValue.ForwardDensityData.gaussian_weight line 26
  4. lemma OAI.SKValue.ForwardDensityData.gaussian_jet line 29
  5. def OAI.SKValue.ForwardDensityData.jump line 34
  6. lemma OAI.SKValue.ForwardDensityData.jump_weight line 49
  7. lemma OAI.SKValue.ForwardDensityData.jump_jet line 57
  8. lemma OAI.SKValue.ForwardDensityData.jump_slope_concavity line 75
  9. lemma OAI.SKValue.ExpGrowth.const line 101
  10. lemma OAI.SKValue.ExpGrowth.add line 103
  11. lemma OAI.SKValue.ExpGrowth.neg line 113
  12. lemma OAI.SKValue.ExpGrowth.sub line 115
  13. lemma OAI.SKValue.ExpGrowth.mul line 117
  14. lemma OAI.SKValue.ExpGrowth.pow line 127
  15. lemma OAI.SKValue.ExpGrowth.abs line 131
  16. lemma OAI.SKValue.ExpGrowth.gaussian_integrable line 133
  17. lemma OAI.SKValue.ExpGrowth.pdf_integrable line 137