OAI/Probability/SKFluctuations/RescaledProfileTestContinuity.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Rescaled Profile Test Continuity.

  1. def OAI.SKFluctuations.Hierarchy.rescaledBoundedProfile line 21
  2. theorem OAI.SKFluctuations.Hierarchy.continuous_rescaledBoundedProfile line 25
  3. theorem OAI.SKFluctuations.Hierarchy.boundedNonnegativeProfile_rescaled line 31
  4. theorem OAI.SKFluctuations.Hierarchy.continuous_rescaledProfile_test line 34
  5. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_rescaled_test_tendsto line 41
  6. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixResidualApproximation line 63
  7. def OAI.SKFluctuations.Hierarchy.scalarPrefixRootSecond line 123
  8. def OAI.SKFluctuations.Hierarchy.scalarPrefixRootThird line 132
  9. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixRoot_transversality line 141
  10. theorem OAI.SKFluctuations.Hierarchy.realSpatialJet_congr_slice line 178
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_zero_congr line 187
  12. theorem OAI.SKFluctuations.Hierarchy.scalarPlateau_test_concat line 196
  13. theorem OAI.SKFluctuations.Hierarchy.ScalarPlateauRoot_plateauRoot_jet line 259
  14. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixRootSecond_plateau line 271
  15. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixRootThird_plateau line 295
  16. theorem OAI.SKFluctuations.Hierarchy.scalarPlateau_root_transversality line 323
  17. def OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet line 345
  18. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_continuous line 349
  19. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_bounded line 354
  20. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_smooth line 360
  21. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_line line 365
  22. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_coord line 371
  23. def OAI.SKFluctuations.Hierarchy.scalarTailTestJet line 377
  24. def OAI.SKFluctuations.Hierarchy.scalarTailTestFamily line 389
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.H_congr_F line 410
  26. def OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature line 419
  27. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_plateau line 425
  28. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_derivative_plateau line 451
  29. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_derivative_plateau line 459
  30. theorem OAI.SKFluctuations.Hierarchy.boundedProfile_L1_tendsto line 487
  31. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_parameter_tendstoUniformly line 506
  32. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_parameter_tendsto line 521
  33. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_parameter_tendsto line 541
  34. theorem OAI.SKFluctuations.Hierarchy.tendstoUniformly_squared_unit line 563
  35. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_H_abs_le line 576
  36. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_bounds line 581
  37. theorem OAI.SKFluctuations.Hierarchy.scalarTailSpatialJet_window_tendsto line 597
  38. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_continuous line 612
  39. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedCurvature_parameter_tendsto line 632
  40. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_parameter_tendsto line 651