OAI/Probability/SKFluctuations/Terminal.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Terminal.

  1. def OAI.SKFluctuations.Hierarchy.SourceContinuation.terminal line 23
  2. abbrev OAI.SKFluctuations.Hierarchy.GaussianStep line 85
  3. def OAI.SKFluctuations.Hierarchy.OrderedSteps line 87
  4. def OAI.SKFluctuations.Hierarchy.gaussianHierarchy line 92
  5. def OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean line 100
  6. def OAI.SKFluctuations.Hierarchy.SourceContinuation.weaken line 109
  7. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_source line 129
  8. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_hessian_bounds line 157
  9. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.hasDerivAt_line line 183
  10. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.lineDeriv_smooth line 193
  11. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.lineDeriv_add line 204
  12. def OAI.SKFluctuations.Hierarchy.BddSmooth.lineDerivLinear line 241
  13. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.lineDeriv_pi line 249
  14. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.uniform_first_bound line 262
  15. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.second_pi line 277
  16. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.uniform_second_bound line 289
  17. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_regular line 316
  18. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_integrable line 323
  19. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_smooth line 331
  20. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_hasDerivAt line 343
  21. def OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse line 353
  22. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_smooth line 367
  23. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_hasDerivAt line 388
  24. def OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian line 434
  25. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_eq_lineDeriv line 438
  26. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_symm line 449
  27. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_add_right line 473
  28. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_smul_right line 481
  29. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_add_left line 489
  30. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_smul_left line 499
  31. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_bounds line 508
  32. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_nonneg line 526
  33. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_block_nonneg line 537
  34. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.compCLM line 561
  35. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_sum_left line 575
  36. def OAI.SKFluctuations.Hierarchy.driverMean line 590
  37. def OAI.SKFluctuations.Hierarchy.driverSource line 594
  38. def OAI.SKFluctuations.Hierarchy.driverObservable line 600
  39. theorem OAI.SKFluctuations.Hierarchy.driverMean_smooth line 606
  40. theorem OAI.SKFluctuations.Hierarchy.driverObservable_smooth line 613
  41. theorem OAI.SKFluctuations.Hierarchy.driverMean_hasDerivAt line 626
  42. theorem OAI.SKFluctuations.Hierarchy.driverObservable_hasDerivAt line 635
  43. def OAI.SKFluctuations.Hierarchy.driverEnergy line 661
  44. theorem OAI.SKFluctuations.Hierarchy.driverEnergy_eq line 668
  45. theorem OAI.SKFluctuations.Hierarchy.driverEnergy_smooth line 687