OAI/Probability/SKFluctuations/BackwardClockDerivative.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Backward Clock Derivative.

  1. theorem OAI.SKFluctuations.Hierarchy.clockTest_sub_test line 19
  2. theorem OAI.SKFluctuations.Hierarchy.HeatJet.tested_trace_eq_rate line 27
  3. theorem OAI.SKFluctuations.Hierarchy.HeatJet.backward_cancellation line 37
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.hasDerivAt_backwardTest line 50
  5. theorem OAI.SKFluctuations.Hierarchy.power_increment_le line 81
  6. theorem OAI.SKFluctuations.Hierarchy.sum_power_increment_le line 89
  7. theorem OAI.SKFluctuations.Hierarchy.power_sum_increment_le line 100
  8. def OAI.SKFluctuations.Hierarchy.finiteCompensator line 113
  9. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_zero line 117
  10. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_succ line 121
  11. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_predictable line 127
  12. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_monotone line 138
  13. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_power_exchange line 160
  14. theorem OAI.SKFluctuations.Hierarchy.natPower_support line 210
  15. theorem OAI.SKFluctuations.Hierarchy.integer_young line 222
  16. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_moment_bound line 243
  17. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_measurable line 280
  18. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_bound line 290
  19. theorem OAI.SKFluctuations.Hierarchy.finiteCompensator_power_integrable line 304
  20. theorem OAI.SKFluctuations.Hierarchy.boundedSubmartingale_compensator_moment line 313
  21. def OAI.SKFluctuations.Hierarchy.BoundaryTree.chain line 345
  22. def OAI.SKFluctuations.Hierarchy.BoundaryTree.chainEquiv line 350
  23. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.chain_weight line 356
  24. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.chain_budget line 369
  25. theorem OAI.SKFluctuations.Hierarchy.prefixTest_potential_stability line 375
  26. def OAI.SKFluctuations.Hierarchy.terminalPerturb line 429
  27. theorem OAI.SKFluctuations.Hierarchy.terminalPerturb_lipschitz line 432
  28. theorem OAI.SKFluctuations.Hierarchy.terminalPerturb_parametric line 437
  29. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_terminal_deriv line 447
  30. theorem OAI.SKFluctuations.Hierarchy.prefixTest_terminal_lipschitz_bound line 456
  31. theorem OAI.SKFluctuations.Hierarchy.prefixTest_terminal_lipschitz line 471
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.test_lipschitz line 490
  33. def OAI.SKFluctuations.Hierarchy.HeatJet.terminalPerturb line 515
  34. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_F_prefix line 539
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_A_prefix line 548
  36. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_terminal_deriv line 557