OAI/Probability/SKFluctuations/ScalarParisiValueDiracDyadic.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Scalar Parisi Value Dirac Dyadic.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_dirac_dyadic line 21
  2. theorem OAI.SKFluctuations.Hierarchy.scalarParisiMinimum_neg line 53
  3. theorem OAI.SKFluctuations.Scalar.clamped_nonpos_of_concave_second line 75
  4. theorem OAI.SKFluctuations.Scalar.no_clamped_nonnegative_gap line 122
  5. theorem OAI.SKFluctuations.Scalar.no_clamped_gap_of_fourth_negative line 159
  6. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_mono line 179
  7. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_nonneg line 185
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.abs_expect_le_expect_abs line 191
  9. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.Preserves line 202
  10. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.fresh_preserves line 207
  11. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.step_preserves line 215
  12. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.left_preserves line 228
  13. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.right_preserves line 237
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.attach_preserves line 247
  15. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.normalizedAttach_preserves line 269
  16. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.expect_abs_mul_le line 284
  17. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_relative_abs_le line 300
  18. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_relative_abs_le line 332
  19. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_abs_le_mul line 372
  20. theorem OAI.SKFluctuations.Hierarchy.relative_derivative_exp_bound_on line 388
  21. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_abs_sub_le line 446
  22. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.weight_smooth_static line 460
  23. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.weight_nonneg_static line 478
  24. def OAI.SKFluctuations.Hierarchy.BoundaryTree.expWeight line 492
  25. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.expWeight_step line 497
  26. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.expWeight_fork line 522
  27. theorem OAI.SKFluctuations.Hierarchy.exp_mul_le_exp_mul_of_abs_sub line 544
  28. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.expWeight_le line 553
  29. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.finite_relative line 633