OAI/Probability/SKFluctuations/MomentNorm.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Moment Norm.

  1. def OAI.SKFluctuations.Hierarchy.momentNorm line 21
  2. theorem OAI.SKFluctuations.Hierarchy.momentNorm_nonneg line 25
  3. theorem OAI.SKFluctuations.Hierarchy.momentNorm_eq line 27
  4. theorem OAI.SKFluctuations.Hierarchy.momentNorm_rpow line 35
  5. theorem OAI.SKFluctuations.Hierarchy.momentNorm_mono line 40
  6. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.abs_rpow_zero line 46
  7. theorem OAI.SKFluctuations.Hierarchy.momentNorm_holder line 54
  8. theorem OAI.SKFluctuations.Hierarchy.norm_power_step line 79
  9. theorem OAI.SKFluctuations.Hierarchy.momentNorm_two_sq line 112
  10. theorem OAI.SKFluctuations.Hierarchy.momentNorm_half_pow line 117
  11. theorem OAI.SKFluctuations.Hierarchy.momentNorm_nonneg_one line 126
  12. theorem OAI.SKFluctuations.Hierarchy.momentNorm_recurrence line 131
  13. theorem OAI.SKFluctuations.Hierarchy.real_moment_constant line 147
  14. theorem OAI.SKFluctuations.Hierarchy.bl_real_moment_bound line 185
  15. theorem OAI.SKFluctuations.Hierarchy.bl_centered_moment_bound line 211
  16. theorem OAI.SKFluctuations.Hierarchy.PinFrame.energy_nonneg line 236
  17. theorem OAI.SKFluctuations.Hierarchy.pinnedEnergy_nonneg line 241
  18. theorem OAI.SKFluctuations.Hierarchy.pinnedPotential_continuous line 247
  19. theorem OAI.SKFluctuations.Hierarchy.pinned_centered_moment_le line 259
  20. def OAI.SKFluctuations.Hierarchy.plantedTransitionDensity line 285
  21. theorem OAI.SKFluctuations.Hierarchy.plantedTransitionDensity_eq line 288
  22. theorem OAI.SKFluctuations.Hierarchy.plantedTransitionDensity_integrable line 295
  23. theorem OAI.SKFluctuations.Hierarchy.integral_plantedTransitionDensity line 305
  24. theorem OAI.SKFluctuations.Hierarchy.lintegral_plantedTransitionDensity line 311
  25. theorem OAI.SKFluctuations.Hierarchy.plantedTransitionLaw_eq line 318
  26. def OAI.SKFluctuations.Hierarchy.standardDrivers line 333
  27. instance OAI.SKFluctuations.Hierarchy.(instance at line 336) line 336
  28. def OAI.SKFluctuations.Hierarchy.scaleDriver line 338
  29. theorem OAI.SKFluctuations.Hierarchy.scaleDriver_apply line 342
  30. theorem OAI.SKFluctuations.Hierarchy.scaleDriver_gaussian line 345
  31. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_lipschitz line 361
  32. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_continuous line 368
  33. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_exp_integrable line 374
  34. theorem OAI.SKFluctuations.Hierarchy.lintegral_scaled_transition line 382
  35. theorem OAI.SKFluctuations.Hierarchy.lintegral_fin_cons line 402
  36. def OAI.SKFluctuations.Hierarchy.forwardWeight line 426
  37. def OAI.SKFluctuations.Hierarchy.forwardEnd line 433
  38. theorem OAI.SKFluctuations.Hierarchy.forwardEnd_eq_sum line 439
  39. theorem OAI.SKFluctuations.Hierarchy.measurable_forwardEnd line 446
  40. theorem OAI.SKFluctuations.Hierarchy.measurable_forwardWeight line 453
  41. theorem OAI.SKFluctuations.Hierarchy.lintegral_forwardWeight line 469
  42. theorem OAI.SKFluctuations.Hierarchy.sum_lintegral_forward_terminal line 496
  43. def OAI.SKFluctuations.Hierarchy.hierarchyIncrements line 523
  44. def OAI.SKFluctuations.Hierarchy.hierarchyTransitions line 530
  45. theorem OAI.SKFluctuations.Hierarchy.hierarchyIncrements_measurable line 537
  46. theorem OAI.SKFluctuations.Hierarchy.hierarchyTransitions_measurable line 545
  47. theorem OAI.SKFluctuations.Hierarchy.hierarchyTransitions_normalized line 562
  48. def OAI.SKFluctuations.Hierarchy.hierarchyPathLog line 574
  49. def OAI.SKFluctuations.Hierarchy.hierarchyPathCost line 583
  50. theorem OAI.SKFluctuations.Hierarchy.hierarchyPathWeight_eq line 590
  51. theorem OAI.SKFluctuations.Hierarchy.hierarchyPathLog_telescope line 603
  52. def OAI.SKFluctuations.Hierarchy.hierarchyJointDensity line 621
  53. theorem OAI.SKFluctuations.Hierarchy.hierarchyJointDensity_eq line 626
  54. theorem OAI.SKFluctuations.Hierarchy.hierarchyJointDensity_pos line 643
  55. theorem OAI.SKFluctuations.Hierarchy.hierarchyJointDensity_normalized line 649