OAI/Probability/SKFluctuations/GaussianSmallScale.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Small Scale.

  1. theorem OAI.SKFluctuations.Hierarchy.gaussianReal_sqrt_rescale line 19
  2. theorem OAI.SKFluctuations.Hierarchy.gaussianKernel_integral_rescale line 28
  3. theorem OAI.SKFluctuations.Hierarchy.gaussianStandard_sq_integral line 37
  4. theorem OAI.SKFluctuations.Hierarchy.gaussianStandard_expabs_sq_integrable line 42
  5. theorem OAI.SKFluctuations.Hierarchy.gaussianSmallScale_dominated_limit line 64
  6. theorem OAI.SKFluctuations.Hierarchy.gaussianLinearEnvelopeMass_rescale line 120
  7. theorem OAI.SKFluctuations.Hierarchy.gaussianLinearEnvelopeMass_tendsto line 131
  8. def OAI.SKFluctuations.Hierarchy.scalarThirdGaussianEnvelope line 143
  9. theorem OAI.SKFluctuations.Hierarchy.scalarThirdGaussianEnvelope_rescale line 148
  10. theorem OAI.SKFluctuations.Hierarchy.scalarThirdGaussianEnvelope_tendsto line 175
  11. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_prefix line 201
  12. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_block_upper line 211
  13. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_block_lower line 254
  14. theorem OAI.SKFluctuations.Hierarchy.prefixTest_add_const_mul line 308
  15. def OAI.SKFluctuations.Hierarchy.hierarchyBlockVariance line 328
  16. def OAI.SKFluctuations.Hierarchy.hierarchyBlockHessianDrop line 335
  17. theorem OAI.SKFluctuations.Hierarchy.hierarchyBlockHessianDrop_bounds line 341
  18. theorem OAI.SKFluctuations.Hierarchy.hierarchyBlockHessianDrop_nonneg line 361
  19. theorem OAI.SKFluctuations.Hierarchy.hierarchyBlockVariance_eq_integral line 381
  20. theorem OAI.SKFluctuations.Hierarchy.hierarchyBlockVariance_nonneg line 410
  21. abbrev OAI.SKFluctuations.Hierarchy.GaussianLayer line 428
  22. def OAI.SKFluctuations.Hierarchy.layerSteps line 430
  23. def OAI.SKFluctuations.Hierarchy.hierarchyLayerBound line 433
  24. theorem OAI.SKFluctuations.Hierarchy.hierarchyBlockVariance_smooth line 440
  25. theorem OAI.SKFluctuations.Hierarchy.hierarchyLayerBound_smooth line 454
  26. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_le_layers line 468
  27. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_sum_right line 504
  28. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_sum_bound line 512
  29. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_fork_layer_bound line 537
  30. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_sq_submartingale line 558
  31. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_compensator_moment line 576
  32. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_conditional_square_increment line 601