OAI/Probability/SKFluctuations/ScalarGeneralHeadBalance.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Scalar General Head Balance.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_head_derivative_lower line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_head_balance line 54
  3. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_restart line 86
  4. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_admissible line 105
  5. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_gradientTest line 109
  6. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_error line 112
  7. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_flatten_bound line 135
  8. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_flatten_endpoint_bound line 178
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.G_congr_F line 212
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledSquare_congr line 220
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledSquare_evolve line 228
  12. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_constant_evolve line 247
  13. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_prefix_square line 268
  14. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_prefix_integral line 283
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_terminal_tendsto line 309
  16. def OAI.SKFluctuations.Scalar.UniformSpatialTail line 340
  17. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.zero line 346
  18. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.add line 350
  19. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.neg line 360
  20. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.sub line 365
  21. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.const_mul line 369
  22. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.div_const line 378
  23. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.mul line 382
  24. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.pow_succ line 392
  25. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.lower line 398
  26. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.lower_half line 404
  27. theorem OAI.SKFluctuations.Scalar.second_deriv_nonneg_at_min line 420
  28. theorem OAI.SKFluctuations.Scalar.hasDerivAt_nonpos_at_right_min line 431
  29. theorem OAI.SKFluctuations.Scalar.parabolic_nonneg line 444
  30. theorem OAI.SKFluctuations.Scalar.parabolic_lower_bound line 541
  31. theorem OAI.SKFluctuations.Scalar.parabolic_nonneg_real line 584
  32. theorem OAI.SKFluctuations.Scalar.parabolic_nonneg_halfline line 619