OAI/Probability/SKFluctuations/ScalarFlattenCurvature.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Scalar Flatten Curvature.

  1. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalar_derivA line 19
  2. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalar_derivA₁ line 25
  3. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_gradient_difference line 35
  4. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_curvature_difference line 61
  5. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_flatten_curvature_hasDerivWithinAt line 95
  6. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_origin_flatten_curvature_stationary line 133
  7. theorem OAI.SKFluctuations.Hierarchy.right_deriv_mul_continuous line 150
  8. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_origin_curvature_hasDerivWithinAt line 161
  9. def OAI.SKFluctuations.Hierarchy.rightSlope line 202
  10. theorem OAI.SKFluctuations.Hierarchy.rightSlope_continuousWithinAt line 205
  11. theorem OAI.SKFluctuations.Hierarchy.exists_small_upper_triangle_within line 216
  12. def OAI.SKFluctuations.Hierarchy.scalarTailSecondRate line 246
  13. theorem OAI.SKFluctuations.Hierarchy.scalarTailSecondRate_continuous line 258
  14. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_three_zero line 277
  15. theorem OAI.SKFluctuations.Hierarchy.scalarTailSecondRate_zero line 285
  16. theorem OAI.SKFluctuations.Hierarchy.scalarTail_observedRate_trace line 310
  17. theorem OAI.SKFluctuations.Hierarchy.scalarTailSecondRate_eq line 354
  18. def OAI.SKFluctuations.Hierarchy.scalarHeadSecondRate line 401
  19. theorem OAI.SKFluctuations.Hierarchy.scalarHeadSecondRate_continuous line 405
  20. theorem OAI.SKFluctuations.Hierarchy.scalarHeadSecondRate_zero line 418
  21. theorem OAI.SKFluctuations.Hierarchy.scalarHeadObservedRatio_second_expansion line 429
  22. theorem OAI.SKFluctuations.Hierarchy.exists_small_upper_triangle line 467
  23. theorem OAI.SKFluctuations.Hierarchy.exists_small_right_interval line 488
  24. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_upper_head_obstruction line 500
  25. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_origin_curvature_ge line 544
  26. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_lower_head_obstruction line 558
  27. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_origin_atom_marginality line 588
  28. theorem OAI.SKFluctuations.Hierarchy.weighted_head_integral_continuousOn line 613
  29. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_head_variation line 644