OAI/Probability/SKBarriers/Gaussian/GaussianSpinTrace.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.trace_mul_nonneg_of_posSemidef line 24
  2. theorem OAI.SK.Analytic.trace_mul_mono_of_posSemidef line 33
  3. theorem OAI.SK.Analytic.posSemidef_trace_one_sub line 39
  4. theorem OAI.SK.Analytic.posSemidef_scalar_one_sub line 62
  5. theorem OAI.SK.Analytic.trace_square_bound line 71
  6. def OAI.SK.Analytic.covarianceMatrix line 89
  7. theorem OAI.SK.Analytic.covarianceMatrix_isHermitian line 93
  8. theorem OAI.SK.Analytic.covarianceMatrix_posSemidef line 98
  9. def OAI.SK.Analytic.crossCovarianceMatrix line 118
  10. theorem OAI.SK.Analytic.covarianceMatrix_residual line 123
  11. theorem OAI.SK.Analytic.covariance_stein_bound line 137
  12. theorem OAI.SK.Analytic.conditional_covariance_trace_bound line 166
  13. def OAI.SK.Analytic.finiteMean line 189
  14. def OAI.SK.Analytic.finiteCovariance line 191
  15. theorem OAI.SK.Analytic.finiteMean_apply line 195
  16. theorem OAI.SK.Analytic.finiteCovariance_apply line 199
  17. theorem OAI.SK.Analytic.finiteCovariance_centered line 205
  18. theorem OAI.SK.Analytic.finiteCovariance_posSemidef line 218
  19. theorem OAI.SK.Analytic.finiteMean_dotProduct line 226
  20. theorem OAI.SK.Analytic.finiteCovariance_quadratic line 230
  21. theorem OAI.SK.Analytic.finiteCovariance_trace_le line 244
  22. theorem OAI.SK.Analytic.directionalGradient_coordinateVector line 268
  23. theorem OAI.SK.Analytic.hessian_tilted_integrable line 273
  24. theorem OAI.SK.Analytic.covarianceMatrix_quadratic line 289
  25. theorem OAI.SK.Analytic.gaussianResponse_quadratic line 305
  26. def OAI.SK.Analytic.integratedWeights line 354
  27. theorem OAI.SK.Analytic.integratedWeights_nonneg line 357
  28. theorem OAI.SK.Analytic.integratedWeights_sum line 360
  29. theorem OAI.SK.Analytic.integral_weighted_sum line 367
  30. theorem OAI.SK.Analytic.integratedWeights_total_variance line 372
  31. def OAI.SK.Analytic.cascadeLiftCLM line 398
  32. theorem OAI.SK.Analytic.cascadeLiftCLM_apply line 403
  33. theorem OAI.SK.Analytic.cascadeAffine_gradient_scaled line 408
  34. theorem OAI.SK.Analytic.cascadeAffine_curvature_scaled line 419
  35. theorem OAI.SK.Analytic.cascade_coordinates_field line 448
  36. theorem OAI.SK.Analytic.gaussianResponse_mixture_domination line 470
  37. theorem OAI.SK.Analytic.cascadeGaussianResponse_domination line 508
  38. theorem OAI.SK.Analytic.cascadeGaussian_conditional_trace line 540