OAI/Probability/SKFluctuations/ScalarFlattenedContinuity.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Scalar Flattened Continuity.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarFlattenedEnergy_tendsto line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixTest_envelope line 53
  3. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_origin_curvature_derivative line 114
  4. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_zero_mass_curvature_derivative line 158
  5. def OAI.SKFluctuations.Hierarchy.scalarInitialDensityConstant line 173
  6. theorem OAI.SKFluctuations.Hierarchy.scalarInitialDensityConstant_pos line 177
  7. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedThirdSquare_envelope line 198
  8. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedThirdSquare_initial_limit line 216
  9. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedJetPower_zero line 238
  10. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_cdf_initial_limit line 246
  11. def OAI.SKFluctuations.Hierarchy.scalarQuantile line 281
  12. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_level_nonempty line 284
  13. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_level_nonneg line 290
  14. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_level_bddBelow line 297
  15. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_cdf_ge line 301
  16. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_le_iff line 316
  17. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_nonneg line 324
  18. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_monotoneOn line 329
  19. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_pos line 334
  20. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_le_support_top line 342
  21. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_continuousOn line 359
  22. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_quantile_regular line 403
  23. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_regular_support line 426
  24. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_eq_of_rightContinuous line 458
  25. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_cdf_eq line 464
  26. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_tendsto_zero line 477
  27. theorem OAI.SKFluctuations.Hierarchy.scalarQuantile_tendsto_zero_right line 502
  28. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_quantile_initial_limit line 523
  29. theorem OAI.SKFluctuations.Hierarchy.scalarSupport_quantile_linear_bounds line 549
  30. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_linear_quantile line 576