OAI/Probability/SKFluctuations/Bounds.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Bounds.

  1. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.bounds line 21
  2. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_abs_mono line 27
  3. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_mono line 41
  4. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_nonneg line 54
  5. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_abs_mono line 61
  6. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_abs_le line 81
  7. def OAI.SKFluctuations.Hierarchy.ProductTree.abs line 88
  8. theorem OAI.SKFluctuations.Hierarchy.ProductTree.abs_mean_nonneg line 92
  9. theorem OAI.SKFluctuations.Hierarchy.ProductTree.mean_abs_le line 103
  10. inductive OAI.SKFluctuations.Hierarchy.ReplicaTree line 128
  11. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Assignment line 136
  12. def OAI.SKFluctuations.Hierarchy.ReplicaTree.assignmentFintype line 141
  13. def OAI.SKFluctuations.Hierarchy.ReplicaTree.leaves line 148
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.leaves_pos line 153
  15. def OAI.SKFluctuations.Hierarchy.ReplicaTree.weight line 164
  16. def OAI.SKFluctuations.Hierarchy.ReplicaTree.expect line 172
  17. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_smooth line 176
  18. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.mul_const line 188
  19. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_smooth line 193
  20. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_finsetSum line 199
  21. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_const line 214
  22. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_step line 222
  23. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_nonneg line 238
  24. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_sum line 249
  25. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_abs_le line 265
  26. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_add line 285
  27. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_const_mul line 290
  28. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_finsetSum line 298
  29. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_fork line 305
  30. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_fork_product line 311
  31. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_indicator line 322
  32. def OAI.SKFluctuations.Hierarchy.ReplicaTree.single line 335
  33. def OAI.SKFluctuations.Hierarchy.ReplicaTree.singleEquiv line 339
  34. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.single_leaves line 343
  35. structure OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement line 350
  36. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.fresh line 356
  37. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.coincide line 362
  38. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.step line 368
  39. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.left line 375
  40. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.right line 382
  41. def OAI.SKFluctuations.Hierarchy.ReplicaTree.attach line 391
  42. def OAI.SKFluctuations.Hierarchy.ReplicaTree.variation line 398
  43. def OAI.SKFluctuations.Hierarchy.ReplicaTree.mass line 401
  44. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.attach_mass line 404
  45. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.attach_variation line 420
  46. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.attach_leaves line 442
  47. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.eval line 474
  48. def OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList line 479
  49. def OAI.SKFluctuations.Hierarchy.ReplicaTree.row line 484
  50. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_add line 488
  51. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_const_mul line 505
  52. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_finsetSum line 520
  53. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_indicator_expand line 529
  54. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.eval_left line 539
  55. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.eval_right line 553
  56. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_map_left line 560
  57. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_map_right line 572
  58. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_smooth line 586
  59. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_abs_le line 594
  60. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.row_abs_le line 615
  61. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.single_expect line 622
  62. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.eval_fresh line 639