OAI/Probability/GaussianPropeller/SoftMinimum.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.SoftMin.Z line 29
  2. def OAI.GaussianPropeller.SoftMin.weight line 30
  3. def OAI.GaussianPropeller.SoftMin.value line 31
  4. def OAI.GaussianPropeller.SoftMin.grad line 32
  5. def OAI.GaussianPropeller.SoftMin.hess line 33
  6. lemma OAI.GaussianPropeller.SoftMin.Z_pos line 36
  7. lemma OAI.GaussianPropeller.SoftMin.weight_pos line 38
  8. lemma OAI.GaussianPropeller.SoftMin.sum_weight line 40
  9. lemma OAI.GaussianPropeller.SoftMin.continuous_Z line 44
  10. lemma OAI.GaussianPropeller.SoftMin.continuous_weight line 45
  11. lemma OAI.GaussianPropeller.SoftMin.continuous_grad line 48
  12. lemma OAI.GaussianPropeller.SoftMin.continuous_hess line 51
  13. lemma OAI.GaussianPropeller.SoftMin.inner_grad line 59
  14. lemma OAI.GaussianPropeller.SoftMin.Z_fderiv line 62
  15. lemma OAI.GaussianPropeller.SoftMin.value_fderiv line 77
  16. lemma OAI.GaussianPropeller.SoftMin.weight_fderiv line 81
  17. lemma OAI.GaussianPropeller.SoftMin.grad_fderiv line 94
  18. lemma OAI.GaussianPropeller.SoftMin.grad_bound line 102
  19. lemma OAI.GaussianPropeller.SoftMin.hess_bound line 112
  20. lemma OAI.GaussianPropeller.SoftMin.hess_nonpos line 128
  21. lemma OAI.GaussianPropeller.SoftMin.concave_of_hessian line 152
  22. lemma OAI.GaussianPropeller.SoftMin.value_concave line 180
  23. lemma OAI.GaussianPropeller.SoftMin.value_lipschitz line 183
  24. lemma OAI.GaussianPropeller.SoftMin.value_le_score line 197
  25. lemma OAI.GaussianPropeller.SoftMin.value_tendsto_atBot line 207
  26. lemma OAI.GaussianPropeller.SoftMin.value_tendsto_atTop line 214