OAI/Probability/SKFluctuations/ScalarFullOriginMarginality.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Scalar Full Origin Marginality.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_head_obstruction line 21
  2. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_origin_marginality line 50
  3. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_origin_zero line 77
  4. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_mem_closure_support line 143
  5. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_measure_origin_zero line 164
  6. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_origin_regular line 184
  7. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_rightMass line 211
  8. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_constant_of_support_hole line 216
  9. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_support_interval line 233
  10. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_support_initial_interval line 263
  11. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_one_not_support_rc line 290
  12. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_one_not_support line 330
  13. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_support_eq_initial_interval line 355
  14. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_support_self_consistency line 387
  15. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_interval_support line 409
  16. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_cdf_zero line 437
  17. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_cdf_strictMono line 445
  18. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_cdf_top line 456
  19. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_curvature_marginality line 478
  20. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_support_curvature line 506
  21. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCube_pos line 529
  22. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_cdf_positive line 538
  23. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_flux_zero line 548
  24. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_cdf_ratio line 574
  25. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_cdf_continuousAt line 588
  26. def OAI.SKFluctuations.Hierarchy.scalarThirdSlope line 613
  27. theorem OAI.SKFluctuations.Hierarchy.scalarThirdSlope_continuous line 617
  28. theorem OAI.SKFluctuations.Hierarchy.scalarThirdSlope_zero line 626
  29. theorem OAI.SKFluctuations.Hierarchy.scalarThirdSlope_bound line 632
  30. theorem OAI.SKFluctuations.Hierarchy.scalarThirdSlope_factor line 645