OAI/Probability/LogConcave/Numerics/NodePolynomial.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.Quadrature.zeroNodePolynomial line 15
  2. lemma OAI.LogConcaveSampling.Quadrature.zeroNodePolynomial_eval line 18
  3. lemma OAI.LogConcaveSampling.Quadrature.zeroNodePolynomial_derivative line 27
  4. lemma OAI.LogConcaveSampling.Quadrature.zeroNodePolynomial_derivative_ne line 32
  5. def OAI.LogConcaveSampling.Quadrature.zeroHermiteBasis line 39
  6. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteBasis_eval line 43
  7. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteBasis_derivative_zero line 54
  8. def OAI.LogConcaveSampling.Quadrature.zeroHermitePolynomial line 63
  9. lemma OAI.LogConcaveSampling.Quadrature.zeroHermitePolynomial_eval line 66
  10. lemma OAI.LogConcaveSampling.Quadrature.zeroHermitePolynomial_derivative_zero line 72
  11. lemma OAI.LogConcaveSampling.Quadrature.polynomial_divX_eval line 78
  12. def OAI.LogConcaveSampling.Quadrature.zeroHermiteRegularized line 86
  13. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteRegularized_eval line 89
  14. def OAI.LogConcaveSampling.Quadrature.zeroHermiteWeight line 94
  15. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_weight_finite line 97
  16. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_weights_abs line 101
  17. lemma OAI.LogConcaveSampling.Quadrature.zeroNodePolynomial_natDegree line 119
  18. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteBasis_natDegree line 130
  19. lemma OAI.LogConcaveSampling.Quadrature.zeroHermitePolynomial_degree line 138
  20. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_unique_zero line 145
  21. theorem OAI.LogConcaveSampling.Quadrature.zeroHermite_reproduces line 171
  22. def OAI.LogConcaveSampling.Quadrature.zeroHermiteInterpolation line 198
  23. def OAI.LogConcaveSampling.Quadrature.zeroHermiteAction line 201
  24. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteInterpolation_hasDerivAt line 204
  25. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteInterpolation_derivative_zero line 209
  26. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteAction_continuous line 215
  27. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteAction_eq line 219
  28. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteAction_integral line 226
  29. theorem OAI.LogConcaveSampling.Quadrature.zeroHermiteAction_value_error_rms line 236
  30. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_reproduces_power line 270
  31. theorem OAI.LogConcaveSampling.Quadrature.zeroHermite_reproduces_vector line 283
  32. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_reproduces_chainTaylor line 298
  33. lemma OAI.LogConcaveSampling.Quadrature.zeroHermiteInterpolation_sub line 309
  34. theorem OAI.LogConcaveSampling.Quadrature.zeroHermite_chain_error_eq line 314