OAI/Probability/SKFluctuations/AbsTiltedMeanLe.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Abs Tilted Mean Le.

  1. theorem OAI.SKFluctuations.Hierarchy.abs_tiltedMean_le line 21
  2. def OAI.SKFluctuations.Hierarchy.shiftedMean line 40
  3. def OAI.SKFluctuations.Hierarchy.shiftedContinuation line 43
  4. theorem OAI.SKFluctuations.Hierarchy.continuous_tested_partition line 49
  5. theorem OAI.SKFluctuations.Hierarchy.continuous_shiftedMean line 86
  6. theorem OAI.SKFluctuations.Hierarchy.continuous_shiftedContinuation line 98
  7. def OAI.SKFluctuations.Hierarchy.BddSmooth line 116
  8. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.down line 121
  9. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.continuous line 124
  10. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.bound line 129
  11. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.const line 135
  12. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.add line 141
  13. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.mul line 156
  14. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.const_mul line 174
  15. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.neg line 177
  16. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.sub line 181
  17. def OAI.SKFluctuations.Hierarchy.PotentialRegularity line 186
  18. theorem OAI.SKFluctuations.Hierarchy.PotentialRegularity.down line 190
  19. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_shiftedMean line 204
  20. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.shiftedMean line 228
  21. theorem OAI.SKFluctuations.Hierarchy.lipschitzWith_shiftedContinuation line 261
  22. theorem OAI.SKFluctuations.Hierarchy.PotentialRegularity.shiftedContinuation line 292
  23. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.sum line 317
  24. def OAI.SKFluctuations.Hierarchy.spinPartition line 328
  25. def OAI.SKFluctuations.Hierarchy.spinWeight line 331
  26. def OAI.SKFluctuations.Hierarchy.spinLogPartition line 334
  27. theorem OAI.SKFluctuations.Hierarchy.spinPartition_pos line 337
  28. theorem OAI.SKFluctuations.Hierarchy.continuous_spinPartition line 342
  29. theorem OAI.SKFluctuations.Hierarchy.continuous_spinWeight line 346
  30. theorem OAI.SKFluctuations.Hierarchy.spinWeight_nonneg line 351
  31. theorem OAI.SKFluctuations.Hierarchy.sum_spinWeight line 355
  32. theorem OAI.SKFluctuations.Hierarchy.spinWeight_le_one line 360
  33. theorem OAI.SKFluctuations.Hierarchy.line_derivative_linear line 365
  34. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_spinPartition line 371
  35. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_spinWeight line 376
  36. theorem OAI.SKFluctuations.Hierarchy.bddSmooth_spinWeight line 393
  37. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_spinLogPartition line 409
  38. theorem OAI.SKFluctuations.Hierarchy.lipschitzWith_spinLogPartition line 417
  39. theorem OAI.SKFluctuations.Hierarchy.potentialRegularity_spinLogPartition line 445
  40. def OAI.SKFluctuations.Hierarchy.ExponentialIncrement line 462
  41. theorem OAI.SKFluctuations.Hierarchy.ExponentialIncrement.integrable_shift line 465
  42. theorem OAI.SKFluctuations.Hierarchy.integrable_exp_mul_abs_gaussianReal line 483
  43. theorem OAI.SKFluctuations.Hierarchy.exponentialIncrement_gaussian line 499
  44. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.integrable_shifted_weighted line 529
  45. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_add line 537
  46. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_sub line 545
  47. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_const_mul line 553
  48. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_mono line 557
  49. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_nonneg line 566
  50. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_square_sub_nonneg line 570
  51. structure OAI.SKFluctuations.Hierarchy.SourceContinuation line 587
  52. def OAI.SKFluctuations.Hierarchy.SourceContinuation.step line 608