OAI/Probability/SKFluctuations/ScoreMGF.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Score M G F.

  1. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.integrable_tiltedLaw line 20
  2. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.exp_vectorDot line 36
  3. theorem OAI.SKFluctuations.GaussianCalculus.gaussianVectorScore_exp_expBounded line 42
  4. theorem OAI.SKFluctuations.GaussianCalculus.gaussian_ode_bound line 58
  5. theorem OAI.SKFluctuations.GaussianCalculus.tiltedMean_vectorScore_exp_identity line 93
  6. theorem OAI.SKFluctuations.GaussianCalculus.gaussianVectorScore_hasSubgaussianMGF line 132
  7. theorem OAI.SKFluctuations.Hierarchy.odd_power_gap_le line 203
  8. theorem OAI.SKFluctuations.Hierarchy.odd_power_coercivity line 225
  9. theorem OAI.SKFluctuations.Hierarchy.finite_centered_odd_covariance line 242
  10. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.nonneg line 279
  11. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_odd_coercivity line 285
  12. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_pi line 318
  13. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_linear_components line 336
  14. def OAI.SKFluctuations.Hierarchy.hierarchyAffineScore line 361
  15. theorem OAI.SKFluctuations.Hierarchy.hierarchyAffineScore_eq line 367
  16. theorem OAI.SKFluctuations.Hierarchy.hierarchyAffineScore_hasSubgaussianMGF line 377
  17. theorem OAI.SKFluctuations.Hierarchy.hierarchyAffineScore_even_bound line 406
  18. theorem OAI.SKFluctuations.Hierarchy.tiltedMean_hierarchyAffineScore line 437
  19. def OAI.SKFluctuations.Hierarchy.forwardScore line 490
  20. theorem OAI.SKFluctuations.Hierarchy.measurable_forwardScore line 497
  21. def OAI.SKFluctuations.Hierarchy.forwardLaw line 512
  22. theorem OAI.SKFluctuations.Hierarchy.forwardLaw_isProbability line 516
  23. theorem OAI.SKFluctuations.Hierarchy.lintegral_forwardScore_exp_le line 525
  24. theorem OAI.SKFluctuations.Hierarchy.forwardScore_hasSubgaussianMGF line 587