OAI/Probability/SKFluctuations/ResidualGradientBound.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Residual Gradient Bound.

  1. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.heat_gradient_bound line 19
  2. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.heat_gradient_bound line 30
  3. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.atom_gradient_bound line 40
  4. theorem OAI.SKFluctuations.Hierarchy.ScalarFinitePositivePrefix.density_gradient_bound line 55
  5. theorem OAI.SKFluctuations.Hierarchy.ScalarPrefixDensity.integral line 98
  6. def OAI.SKFluctuations.Hierarchy.gaussianLinearEnvelope line 110
  7. def OAI.SKFluctuations.Hierarchy.gaussianLinearEnvelopeMass line 113
  8. theorem OAI.SKFluctuations.Hierarchy.gaussianLinearEnvelope_integrable line 116
  9. theorem OAI.SKFluctuations.Hierarchy.gaussianLinearEnvelopeMass_pos line 123
  10. theorem OAI.SKFluctuations.Hierarchy.gaussian_tilt_envelope line 138
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_one_absolute_error line 185
  12. theorem OAI.SKFluctuations.Hierarchy.clockExcess_nonpos line 213
  13. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_schedule_reverse_error line 221
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_one_signed_error line 277
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_schedule_signed_error line 309
  16. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_profile_signed_error line 368
  17. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_signed_error line 407
  18. theorem OAI.SKFluctuations.Hierarchy.right_derivative_of_quadratic_remainder line 440
  19. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_hasDerivWithinAt line 470
  20. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_continuous line 503
  21. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_difference line 512
  22. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_initial_value line 530
  23. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_replace_head_general line 542
  24. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_replace_head_general line 571
  25. theorem OAI.SKFluctuations.Hierarchy.parametric_testedPartition_continuous line 611
  26. theorem OAI.SKFluctuations.Hierarchy.parametric_clockTest_continuous line 662