OAI/Probability/FreeIsing/Gaussian/IntegrationByParts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.hasDerivAt_gaussianPDFReal line 12
  2. theorem OAI.Problem367.integrable_gaussian_iff_density line 23
  3. theorem OAI.Problem367.gaussian_integral_centered_mul_eq_variance_mul_deriv line 33
  4. theorem OAI.Problem367.gaussian_integral_centered_mul_of_bounded line 75
  5. theorem OAI.Problem367.gaussian_integral_centered_mul_of_bounded_deriv line 91
  6. theorem OAI.Problem367.gaussian_integral_mul_affine_of_bounded_deriv line 105