OAI/Probability/SKFluctuations/ScalarIntervalPenalty.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Scalar Interval Penalty.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_replace_interval line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_interval_upper line 55
  3. def OAI.SKFluctuations.Hierarchy.scalarIntervalMassValue line 77
  4. theorem OAI.SKFluctuations.Hierarchy.scalarIntervalMassValue_eq line 83
  5. theorem OAI.SKFluctuations.Hierarchy.scalarIntervalMassValue_hasDerivAt line 104
  6. theorem OAI.SKFluctuations.Hierarchy.scalarIntervalMassValue_spillover line 140
  7. theorem OAI.SKFluctuations.Hierarchy.scalarIntervalMassValue_plateau line 188
  8. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_interval_tail_error line 205
  9. theorem OAI.SKFluctuations.Hierarchy.scalarIntervalMassValue_tail_spillover line 271
  10. def OAI.SKFluctuations.Hierarchy.clipLowerProfile line 324
  11. theorem OAI.SKFluctuations.Hierarchy.clipLowerProfile_mem line 343
  12. theorem OAI.SKFluctuations.Hierarchy.clipLowerProfile_before line 354
  13. theorem OAI.SKFluctuations.Hierarchy.clipLowerProfile_after line 360
  14. theorem OAI.SKFluctuations.Hierarchy.clipLowerProfile_flat line 364
  15. theorem OAI.SKFluctuations.Hierarchy.clipLowerProfile_error line 370
  16. def OAI.SKFluctuations.Hierarchy.clipUpperProfile line 389
  17. theorem OAI.SKFluctuations.Hierarchy.clipUpperProfile_mem line 408
  18. theorem OAI.SKFluctuations.Hierarchy.clipUpperProfile_before line 419
  19. theorem OAI.SKFluctuations.Hierarchy.clipUpperProfile_after line 423
  20. theorem OAI.SKFluctuations.Hierarchy.clipUpperProfile_flat line 429
  21. theorem OAI.SKFluctuations.Hierarchy.clipUpperProfile_error line 435
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_profile_reverse_error line 454
  23. theorem OAI.SKFluctuations.Hierarchy.scalarLocalResponse_upper line 503
  24. theorem OAI.SKFluctuations.Hierarchy.scalarInterval_mass_bound line 568
  25. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_local_upper line 577
  26. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_local_lower line 605