OAI/Probability/SKFluctuations/Projection.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Projection.

  1. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.const line 21
  2. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.neg line 25
  3. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.add line 29
  4. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.sub line 41
  5. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.mul line 44
  6. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.const_mul line 55
  7. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.pow line 58
  8. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.integrable line 64
  9. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.sum line 69
  10. def OAI.SKFluctuations.GaussianCalculus.gaussianTiltScore line 85
  11. theorem OAI.SKFluctuations.GaussianCalculus.gaussianTiltScore_expBounded line 87
  12. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_expBounded_mono line 91
  13. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_score line 102
  14. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_score_even_step line 132
  15. def OAI.SKFluctuations.GaussianCalculus.gaussianEvenConstant line 176
  16. theorem OAI.SKFluctuations.GaussianCalculus.gaussianEvenConstant_pos line 180
  17. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_score_even_bound line 185
  18. theorem OAI.SKFluctuations.GaussianCalculus.hierarchy_line_score_bound line 205
  19. def OAI.SKFluctuations.GaussianCalculus.vectorDot line 235
  20. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.vectorDot line 237
  21. theorem OAI.SKFluctuations.GaussianCalculus.standardGaussianVector_directional_stein line 243
  22. def OAI.SKFluctuations.GaussianCalculus.gaussianVectorScore line 271
  23. theorem OAI.SKFluctuations.GaussianCalculus.gaussianVectorScore_expBounded line 275
  24. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_vectorScore line 283
  25. theorem OAI.SKFluctuations.GaussianCalculus.vectorDot_line line 339
  26. theorem OAI.SKFluctuations.GaussianCalculus.vectorDot_single line 348
  27. theorem OAI.SKFluctuations.GaussianCalculus.gaussianVectorScore_hasDerivAt line 351
  28. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_expNormBounded_mono line 366
  29. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_vectorScore_even_step line 377
  30. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_vectorScore_even_bound line 441
  31. theorem OAI.SKFluctuations.Hierarchy.finite_covariance_identity line 477
  32. theorem OAI.SKFluctuations.Hierarchy.finite_covariance_nonneg line 487
  33. def OAI.SKFluctuations.Hierarchy.hierarchyCovariance line 502
  34. theorem OAI.SKFluctuations.Hierarchy.hierarchyCovariance_smooth line 507
  35. theorem OAI.SKFluctuations.Hierarchy.hierarchyCovariance_nonneg line 514
  36. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_comonotone_lower line 526