OAI/Probability/SKFluctuations/ScalarJetPowerTests.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Scalar Jet Power Tests.

  1. theorem OAI.SKFluctuations.Hierarchy.tendstoUniformly_pow_of_abs_le line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_bddSmooth_all line 27
  3. def OAI.SKFluctuations.Hierarchy.scalarJetPowerTest line 33
  4. def OAI.SKFluctuations.Hierarchy.scalarPlantedJetPower line 38
  5. theorem OAI.SKFluctuations.Hierarchy.scalarJetPowerTest_bound line 43
  6. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedJetPower_abs_le line 52
  7. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedJetPower_continuous line 59
  8. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedJetPower_parameter_tendsto line 81
  9. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_zero_all line 111
  10. def OAI.SKFluctuations.Hierarchy.scalarCurvatureFlux line 124
  11. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixRootSecond_eq_flux line 128
  12. theorem OAI.SKFluctuations.Hierarchy.scalarCurvatureFlux_intervalIntegrable line 161
  13. theorem OAI.SKFluctuations.Hierarchy.scalarCurvatureFlux_parameter_tendsto line 167
  14. theorem OAI.SKFluctuations.Hierarchy.scalarCurvatureFlux_right_continuous line 176
  15. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_derivative_flux_plateau line 182
  16. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_grid_integral line 200
  17. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_curvature_integral line 237
  18. theorem OAI.SKFluctuations.Hierarchy.scalarCurvatureFlux_measurable line 266
  19. theorem OAI.SKFluctuations.Hierarchy.scalarCurvatureFlux_abs_le line 272
  20. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_integral line 301
  21. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_right_derivative line 340
  22. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_grid_integral line 370
  23. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_energy_integral line 406
  24. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_integral line 437
  25. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_derivative line 476
  26. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixTest_pos line 501
  27. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_lt_one line 543
  28. theorem OAI.SKFluctuations.Hierarchy.scalarPrefix_error line 574
  29. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_prefix_error line 613