OAI/Probability/SKFluctuations/ScalarZeroPlateau.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Scalar Zero Plateau.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_head_balance_one line 20
  2. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_observedSquare_le_one line 48
  3. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_no_zero_first_gap line 58
  4. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_no_zero_plateau line 79
  5. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_mass_pos line 88
  6. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_origin_accumulates line 109
  7. theorem OAI.SKFluctuations.Hierarchy.scalarHeadVariation_integrable line 145
  8. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_head_variation line 156
  9. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_strict_origin line 176
  10. theorem OAI.SKFluctuations.Hierarchy.integral_pos_of_initial_pos line 193
  11. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_support_strict line 216
  12. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_local_areas line 233
  13. theorem OAI.SKFluctuations.Hierarchy.HasDerivAt.ge_of_right_error line 255
  14. theorem OAI.SKFluctuations.Hierarchy.HasDerivAt.le_of_left_error line 273
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseFamily_gapTest line 291
  16. theorem OAI.SKFluctuations.Hierarchy.scalarMassResponse_physical line 311
  17. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_left_mass_bound line 346
  18. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_left_mass_nonpos line 375
  19. theorem OAI.SKFluctuations.Hierarchy.scalarMassResponse_physical_integral line 410
  20. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_left_integral_nonpos line 425
  21. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_right_mass_bound line 447
  22. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_right_mass_nonneg line 478
  23. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_plateau_right_integral_nonneg line 505
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockTestDerivative_unit_bound line 527
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockDerivative_unit_bound line 567
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockTest_unit_time_bound line 588
  27. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockValue_unit_time_bound line 602
  28. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_varying_mass_terminal_tendsto line 623