OAI/Probability/SKFluctuations/VariableMassClock.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Variable Mass Clock.

  1. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.comp line 19
  2. theorem OAI.SKFluctuations.Hierarchy.parametric_clockTest_continuous_mass line 24
  3. def OAI.SKFluctuations.Hierarchy.unitMassClip line 48
  4. theorem OAI.SKFluctuations.Hierarchy.unitMassClip_continuous line 50
  5. theorem OAI.SKFluctuations.Hierarchy.unitMassClip_bounds line 52
  6. theorem OAI.SKFluctuations.Hierarchy.unitMassClip_eq line 57
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.clockDerivative_continuous_mass line 61
  8. def OAI.SKFluctuations.Hierarchy.scalarTailJetFamily line 122
  9. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_A_zero line 143
  10. def OAI.SKFluctuations.Hierarchy.HeatJet.observedRate line 147
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.observedRate_zero line 151
  12. def OAI.SKFluctuations.Hierarchy.scalarHeadObservedRatio line 160
  13. theorem OAI.SKFluctuations.Hierarchy.scalarHeadObservedRatio_continuous line 164
  14. theorem OAI.SKFluctuations.Hierarchy.scalarHeadObservedRatio_zero line 172
  15. theorem OAI.SKFluctuations.Hierarchy.scalarHeadObservedRatio_eq line 178
  16. def OAI.SKFluctuations.Hierarchy.HeatJet.testAverageRate line 217
  17. theorem OAI.SKFluctuations.Hierarchy.HeatJet.testAverageRate_zero line 221
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.testAverageRate_eq line 226
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.testAverageRate_continuous_mass line 251
  20. def OAI.SKFluctuations.Hierarchy.replaceIntervalProfile line 273
  21. theorem OAI.SKFluctuations.Hierarchy.replaceIntervalProfile_before line 301
  22. theorem OAI.SKFluctuations.Hierarchy.replaceIntervalProfile_inside line 306
  23. theorem OAI.SKFluctuations.Hierarchy.replaceIntervalProfile_after line 311
  24. theorem OAI.SKFluctuations.Hierarchy.replaceIntervalProfile_mem line 316
  25. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_prefix line 336
  26. theorem OAI.SKFluctuations.Hierarchy.scalarPrefix_congr line 349
  27. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_interval_flat line 362
  28. def OAI.SKFluctuations.Hierarchy.scalarFlattenedEnergy line 392
  29. theorem OAI.SKFluctuations.Hierarchy.scalarLocalResponse_lower line 397
  30. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockTest_time_bound line 460
  31. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockValue_time_bound line 473
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockTest_terminal_stability line 484
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_small_terminal_tendsto line 499
  34. theorem OAI.SKFluctuations.Hierarchy.closedSet_gap_endpoints line 546
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_lipschitzOnWith line 570
  36. theorem OAI.SKFluctuations.Hierarchy.lipschitzOnWith_closed_interval_of_derivative_bound line 584
  37. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapEnergy_continuousOn line 595
  38. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapCurvature_continuousOn line 617