OAI/Probability/SKFluctuations/ScalarVaryingFlattenedContinuity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Scalar Varying Flattened Continuity.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarFlattenedEnergy_varying_mass_tendsto line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_support_stationarity line 53
  3. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_KKT line 113
  4. theorem OAI.SKFluctuations.Hierarchy.hasDerivWithinAt_endpoints_of_continuous_derivative line 160
  5. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_plateau_endpoint_derivatives line 182
  6. theorem OAI.SKFluctuations.Hierarchy.HasDerivWithinAt.nonpos_of_right_integral_nonpos line 222
  7. theorem OAI.SKFluctuations.Hierarchy.HasDerivWithinAt.nonpos_of_left_integral_nonneg line 245
  8. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_endpoint_KKT line 284
  9. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_no_positive_support_gap line 323
  10. def OAI.SKFluctuations.Hierarchy.HeatJet.testProduct line 411
  11. def OAI.SKFluctuations.Hierarchy.HeatJetFamily.testProduct line 431
  12. theorem OAI.SKFluctuations.Hierarchy.HeatJet.testAverageRate_zero_scalar line 447
  13. def OAI.SKFluctuations.Hierarchy.scalarTailCurvatureRate line 463
  14. theorem OAI.SKFluctuations.Hierarchy.scalarTailCurvatureRate_continuous line 469
  15. theorem OAI.SKFluctuations.Hierarchy.scalarTailCurvatureRate_zero line 477
  16. theorem OAI.SKFluctuations.Hierarchy.scalarTailCurvatureRate_eq line 493
  17. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_signed_error_source line 523
  18. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_observedSquare_continuous_source line 546
  19. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_hasDerivWithinAt_source line 553
  20. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_continuous_source line 578
  21. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_difference_source line 587
  22. theorem OAI.SKFluctuations.Hierarchy.weighted_profile_integral_hasDerivAt line 615