OAI/Probability/SKFluctuations/WeightedClockPDE.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Weighted Clock P D E.

  1. def OAI.SKFluctuations.Scalar.weightedP line 19
  2. def OAI.SKFluctuations.Scalar.weightedQ line 21
  3. def OAI.SKFluctuations.Scalar.weightedR line 23
  4. theorem OAI.SKFluctuations.Scalar.weightedP_continuous line 30
  5. theorem OAI.SKFluctuations.Scalar.weightedQ_continuous line 36
  6. theorem OAI.SKFluctuations.Scalar.weightedR_continuous line 44
  7. theorem OAI.SKFluctuations.Scalar.weightedP_space line 48
  8. theorem OAI.SKFluctuations.Scalar.weightedP_space_two line 55
  9. theorem OAI.SKFluctuations.Scalar.weightedQ_space line 63
  10. theorem OAI.SKFluctuations.Scalar.weightedQ_space_two line 70
  11. theorem OAI.SKFluctuations.Scalar.weightedR_space line 79
  12. theorem OAI.SKFluctuations.Scalar.weightedR_space_two line 86
  13. theorem OAI.SKFluctuations.Scalar.realJet_two_time line 107
  14. theorem OAI.SKFluctuations.Scalar.realJet_three_time line 112
  15. theorem OAI.SKFluctuations.Scalar.realJet_four_time line 117
  16. theorem OAI.SKFluctuations.Scalar.realJet_five_time line 122
  17. theorem OAI.SKFluctuations.Scalar.weightedP_time line 127
  18. theorem OAI.SKFluctuations.Scalar.weightedQ_time line 137
  19. theorem OAI.SKFluctuations.Scalar.weightedR_time line 148
  20. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet line 170
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_continuous line 177
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_bound line 182
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_line line 187
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_coord line 194
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_one line 202
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_two line 210
  27. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarJetTest line 218
  28. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarJetFamily line 229
  29. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapEnergy line 250
  30. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapCurvature line 254
  31. theorem OAI.SKFluctuations.Hierarchy.ScalarGapEnergy_scalar_jet_two_time line 263
  32. theorem OAI.SKFluctuations.Hierarchy.ScalarGapEnergy_scalar_energy_rate_algebra line 271
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_scalarGapEnergy line 281
  34. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_scalarGapEnergy line 319
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_scalarGapCurvature line 327
  36. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.pow line 352
  37. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.pow line 358
  38. def OAI.SKFluctuations.Hierarchy.HeatJet.gapTest0 line 363
  39. def OAI.SKFluctuations.Hierarchy.HeatJet.gapTest1 line 365
  40. def OAI.SKFluctuations.Hierarchy.HeatJet.gapTest2 line 368
  41. def OAI.SKFluctuations.Hierarchy.HeatJet.gapTimeTest line 372
  42. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapThird line 377
  43. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_smooth0 line 387
  44. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_smooth1 line 390
  45. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_smooth2 line 393
  46. def OAI.SKFluctuations.Hierarchy.HeatJet.gapJet line 398
  47. def OAI.SKFluctuations.Hierarchy.HeatJet.gapFamily line 419
  48. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_time_smooth line 447
  49. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_time_continuous line 458
  50. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_time_bounded line 465
  51. theorem OAI.SKFluctuations.Hierarchy.ScalarGapThird_gap_third_cancellation line 473
  52. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_scalarGapCurvature line 483
  53. theorem OAI.SKFluctuations.Hierarchy.weighted_bounded_integrable line 523
  54. theorem OAI.SKFluctuations.Hierarchy.weighted_bounded_continuous line 528
  55. theorem OAI.SKFluctuations.Hierarchy.weighted_bounded_hasDerivAt line 543
  56. theorem OAI.SKFluctuations.Scalar.realSpatialJet_parity line 568
  57. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledEnergy_eq_scalarGapEnergy line 590
  58. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivWithinAt_scalarGapEnergy_zero line 602
  59. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapCurvature_zero line 619
  60. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockJet_odd_zero line 623
  61. theorem OAI.SKFluctuations.Hierarchy.ScalarGapEndpoint_profG line 637
  62. theorem OAI.SKFluctuations.Hierarchy.ScalarGapEndpoint_profH line 639
  63. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGap_hasDerivAt line 642
  64. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGapEnergy_hasDerivAt line 648
  65. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGap_initial_curvature line 653