OAI/Probability/ParisiFinite/IntegrablePdfMul.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Integrable Pdf Mul.

  1. theorem OAI.SKGaussian.integrable_pdf_mul line 15
  2. theorem OAI.SKGaussian.hasDerivAt_standardDensity line 23
  3. theorem OAI.SKGaussian.integral_mul_eq_integral_deriv line 35
  4. def OAI.SKGaussian.standardLaw line 56
  5. instance OAI.SKGaussian.(instance at line 59) line 59
  6. theorem OAI.SKGaussian.integral_coord_mul_eq line 65
  7. def OAI.SKGaussian.partition line 94
  8. def OAI.SKGaussian.weight line 96
  9. def OAI.SKGaussian.logPartition line 98
  10. def OAI.SKGaussian.finiteMax line 100
  11. theorem OAI.SKGaussian.partition_pos line 102
  12. theorem OAI.SKGaussian.weight_pos line 105
  13. theorem OAI.SKGaussian.sum_weight line 108
  14. theorem OAI.SKGaussian.weight_le_one line 111
  15. theorem OAI.SKGaussian.continuous_partition line 116
  16. theorem OAI.SKGaussian.continuous_weight line 120
  17. theorem OAI.SKGaussian.continuous_logPartition line 125
  18. theorem OAI.SKGaussian.le_finiteMax line 128
  19. theorem OAI.SKGaussian.le_logPartition line 131
  20. theorem OAI.SKGaussian.finiteMax_le_logPartition line 135
  21. theorem OAI.SKGaussian.logPartition_le line 138
  22. theorem OAI.SKGaussian.abs_weight_sum_le line 150
  23. theorem OAI.SKGaussian.hasDerivAt_logPartition line 160
  24. theorem OAI.SKGaussian.hasDerivAt_weight line 168
  25. theorem OAI.SKGaussian.logPartition_abs_le line 178
  26. theorem OAI.SKGaussian.integrable_logPartition line 190
  27. def OAI.SKGaussian.linearField line 201
  28. theorem OAI.SKGaussian.continuous_linearField line 205
  29. theorem OAI.SKGaussian.integrable_coordinate line 210
  30. theorem OAI.SKGaussian.integrable_linearField line 217
  31. theorem OAI.SKGaussian.integrable_weight line 221
  32. theorem OAI.SKGaussian.hasDerivAt_linearField_insert line 230
  33. theorem OAI.SKGaussian.integrable_weight_derivative line 242
  34. theorem OAI.SKGaussian.integrable_coord_weight line 253
  35. theorem OAI.SKGaussian.integral_coord_weight line 263
  36. theorem OAI.SKGaussian.weighted_covariance line 277
  37. theorem OAI.SKGaussian.linearField_combo line 288
  38. def OAI.SKGaussian.rotateCoeff line 294
  39. def OAI.SKGaussian.velocityCoeff line 297
  40. theorem OAI.SKGaussian.hasDerivAt_rotatedField line 301
  41. theorem OAI.SKGaussian.continuous_weightedMean line 311
  42. theorem OAI.SKGaussian.integrable_weightedMean line 318
  43. theorem OAI.SKGaussian.rotated_derivative_bound line 329
  44. theorem OAI.SKGaussian.hasDerivAt_expected_rotated line 352
  45. theorem OAI.SKGaussian.integral_weightedMean_eq line 373
  46. theorem OAI.SKGaussian.pairwise_covariance line 411
  47. theorem OAI.SKGaussian.integral_weightedMean_eq_pairwise line 446
  48. theorem OAI.SKGaussian.rotated_increment_covariance line 456
  49. theorem OAI.SKGaussian.expected_rotated_derivative_nonneg line 477
  50. theorem OAI.SKGaussian.expected_logPartition_le line 500
  51. theorem OAI.SKGaussian.finiteMax_abs_le line 517
  52. theorem OAI.SKGaussian.continuous_finiteMax line 522
  53. theorem OAI.SKGaussian.integrable_finiteMax line 525
  54. theorem OAI.SKGaussian.finiteMax_const_mul line 533
  55. theorem OAI.SKGaussian.linearField_const_mul line 545
  56. theorem OAI.SKGaussian.expected_finiteMax_le line 552
  57. def OAI.SKGaussian.gaussianLaw line 610
  58. instance OAI.SKGaussian.(instance at line 613) line 613
  59. def OAI.SKGaussian.field line 618
  60. theorem OAI.SKGaussian.integrable_field line 622
  61. theorem OAI.SKGaussian.integral_reindex_field line 632
  62. theorem OAI.SKGaussian.expected_field_max_le_of_orthogonal line 654
  63. theorem OAI.SKGaussian.integral_field_inl line 670
  64. theorem OAI.SKGaussian.integral_field_inr line 690
  65. theorem OAI.SKGaussian.expected_field_max_le line 711