OAI/Probability/SKFluctuations/MartingaleCompensatorLp.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Martingale Compensator Lp.

  1. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_compensator_Lp line 21
  2. theorem OAI.SKFluctuations.Hierarchy.boundedDoob_compensator_moment line 40
  3. def OAI.SKFluctuations.Hierarchy.conditionalSquareSum line 58
  4. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_conditionalSquareSum_eq line 62
  5. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_conditionalSquareSum_moment line 76
  6. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_conditionalSquareSum_Lp line 91
  7. theorem OAI.SKFluctuations.Hierarchy.boundedDoob_conditionalSquareSum_Lp line 108
  8. def OAI.SKFluctuations.Scalar.slopeTangent line 126
  9. theorem OAI.SKFluctuations.Scalar.fderiv_apply_eq_partials line 144
  10. def OAI.SKFluctuations.Scalar.inverseSlope line 151
  11. def OAI.SKFluctuations.Scalar.inverseSlopeMap line 154
  12. theorem OAI.SKFluctuations.Scalar.inverseSlope_left line 157
  13. theorem OAI.SKFluctuations.Scalar.ImplicitSlope_slopeMap_hasFDerivAt line 161
  14. theorem OAI.SKFluctuations.Scalar.inverseSlopeMap_hasFDerivAt line 172
  15. theorem OAI.SKFluctuations.Scalar.inverseSlopeMap_contDiffAt line 188
  16. theorem OAI.SKFluctuations.Scalar.inverseSlope_time_hasDerivAt line 205
  17. theorem OAI.SKFluctuations.Scalar.inverseSlope_space_hasDerivAt line 218
  18. theorem OAI.SKFluctuations.Hierarchy.monotone_initial_ratio_uniform_bounds line 240
  19. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedGapCurvature_root line 288
  20. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedSquare_bound line 329
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedSquare_continuous line 335
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedSquare_hasDerivAt line 346
  23. theorem OAI.SKFluctuations.Hierarchy.scalarPlanted_no_stationary_gap line 367
  24. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalRootIntegral_lower line 415
  25. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalRootIntegral_lower_gaussian line 518
  26. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_residual_root_lower line 620