OAI/Probability/SKFluctuations/ClockFlattenSchedule.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Clock Flatten Schedule.

  1. def OAI.SKFluctuations.Hierarchy.clockLength line 19
  2. def OAI.SKFluctuations.Hierarchy.clockExcess line 20
  3. theorem OAI.SKFluctuations.Hierarchy.clockLength_nil line 23
  4. theorem OAI.SKFluctuations.Hierarchy.clockLength_cons line 24
  5. theorem OAI.SKFluctuations.Hierarchy.clockExcess_nil line 26
  6. theorem OAI.SKFluctuations.Hierarchy.clockExcess_cons line 27
  7. theorem OAI.SKFluctuations.Hierarchy.clockLength_nonneg line 30
  8. theorem OAI.SKFluctuations.Hierarchy.clockExcess_nonneg line 35
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_schedule_energy line 43
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_schedule_error line 62
  11. theorem OAI.SKFluctuations.Hierarchy.clockExcess_append line 118
  12. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid_excess line 122
  13. theorem OAI.SKFluctuations.Hierarchy.dyadicLowerSum_abs_sub line 128
  14. theorem OAI.SKFluctuations.Hierarchy.capped_grid_excess_tendsto line 146
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_profile_error line 172
  16. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_constant_head line 221
  17. def OAI.SKFluctuations.Hierarchy.scalarTailJet line 229
  18. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_G_bound line 233
  19. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_G_smooth line 237
  20. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_constant_head line 243
  21. theorem OAI.SKFluctuations.Hierarchy.scalarHead_hasDerivAt line 270
  22. def OAI.SKFluctuations.Hierarchy.replaceHeadProfile line 298
  23. theorem OAI.SKFluctuations.Hierarchy.replaceHeadProfile_mem line 322
  24. theorem OAI.SKFluctuations.Hierarchy.replaceHeadProfile_head line 333
  25. theorem OAI.SKFluctuations.Hierarchy.replaceHeadProfile_tail line 339
  26. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_head_difference line 345
  27. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_F line 385
  28. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_congr line 390
  29. def OAI.SKFluctuations.Hierarchy.scalarHeadValue line 404
  30. theorem OAI.SKFluctuations.Hierarchy.scalarHeadValue_hasDerivAt line 407
  31. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_replace_head line 413
  32. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_head_derivative_nonpos line 429
  33. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_atomic_head_balance line 453
  34. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_error line 480
  35. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_tail_error line 525
  36. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_head_error line 574
  37. def OAI.SKFluctuations.Hierarchy.floorMassProfile line 616
  38. theorem OAI.SKFluctuations.Hierarchy.floorMassProfile_mem line 635
  39. theorem OAI.SKFluctuations.Hierarchy.floorMassProfile_head line 643
  40. theorem OAI.SKFluctuations.Hierarchy.floorMassProfile_tail line 650
  41. theorem OAI.SKFluctuations.Hierarchy.floorMassProfile_bound line 656