OAI/Probability/SKFluctuations/ScalarClockRegularity.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Scalar Clock Regularity.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_bddSmooth_all line 19
  2. theorem OAI.SKFluctuations.Hierarchy.ScalarClockRegularity_clockContinuation_scalar_source line 31
  3. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_scalar_contDiffOn line 48
  4. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_clock_contDiffOn line 92
  5. def OAI.SKFluctuations.Scalar.timePartial line 111
  6. def OAI.SKFluctuations.Scalar.spacePartial line 113
  7. theorem OAI.SKFluctuations.Scalar.hasDerivAt_timePartial line 116
  8. theorem OAI.SKFluctuations.Scalar.hasDerivAt_spacePartial line 121
  9. theorem OAI.SKFluctuations.Scalar.timePartial_contDiffOn line 126
  10. theorem OAI.SKFluctuations.Scalar.spacePartial_contDiffOn line 131
  11. theorem OAI.SKFluctuations.Scalar.hasDerivAt_spacePartial_time line 137
  12. def OAI.SKFluctuations.Scalar.spatialJet line 165
  13. theorem OAI.SKFluctuations.Scalar.spatialJet_contDiffOn line 169
  14. theorem OAI.SKFluctuations.Scalar.spatialJet_hasDerivAt line 176
  15. theorem OAI.SKFluctuations.Scalar.spacePartial_hasDerivAt_time_of_timePDE line 185
  16. theorem OAI.SKFluctuations.Scalar.spatialJet_one_timePDE line 203
  17. theorem OAI.SKFluctuations.Scalar.spatialJet_two_timePDE line 218
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalar_derivF line 245
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalar_derivG line 251
  20. def OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane line 261
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_contDiffOn line 264
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_jet_one line 270
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_jet_two line 278
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_timePDE line 291
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_gradient_timePDE line 302
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_curvature_timePDE line 312
  27. def OAI.SKFluctuations.Scalar.SpatialRegular line 333
  28. theorem OAI.SKFluctuations.Scalar.SpatialRegular.const line 340
  29. theorem OAI.SKFluctuations.Scalar.SpatialRegular.add line 345
  30. theorem OAI.SKFluctuations.Scalar.SpatialRegular.mul line 354
  31. theorem OAI.SKFluctuations.Scalar.SpatialRegular.const_mul line 364
  32. theorem OAI.SKFluctuations.Scalar.SpatialRegular.neg line 367
  33. theorem OAI.SKFluctuations.Scalar.SpatialRegular.sub line 371
  34. theorem OAI.SKFluctuations.Scalar.SpatialRegular.spatialDerivative line 375
  35. theorem OAI.SKFluctuations.Scalar.SpatialRegular.hasDerivAt line 384
  36. def OAI.SKFluctuations.Scalar.realSpatialJet line 392
  37. theorem OAI.SKFluctuations.Scalar.realSpatialJet_regular line 396
  38. theorem OAI.SKFluctuations.Scalar.realSpatialJet_continuous line 402
  39. theorem OAI.SKFluctuations.Scalar.realSpatialJet_hasDerivAt line 405
  40. theorem OAI.SKFluctuations.Hierarchy.ScalarClockSpatial_test_source_all line 420
  41. theorem OAI.SKFluctuations.Hierarchy.clockTest_scalar_spatialRegular line 439
  42. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_spatialRegular line 462
  43. theorem OAI.SKFluctuations.Scalar.realSpatialJet_eq_spatialJet line 481
  44. def OAI.SKFluctuations.Scalar.SpatialBounded line 501
  45. theorem OAI.SKFluctuations.Scalar.SpatialBounded.const line 508
  46. theorem OAI.SKFluctuations.Scalar.SpatialBounded.add line 513
  47. theorem OAI.SKFluctuations.Scalar.SpatialBounded.mul line 522
  48. theorem OAI.SKFluctuations.Scalar.SpatialBounded.const_mul line 532
  49. theorem OAI.SKFluctuations.Scalar.SpatialBounded.neg line 535
  50. theorem OAI.SKFluctuations.Scalar.SpatialBounded.sub line 539
  51. theorem OAI.SKFluctuations.Scalar.SpatialBounded.spatialDerivative line 543
  52. theorem OAI.SKFluctuations.Scalar.SpatialBounded.regular line 552
  53. theorem OAI.SKFluctuations.Scalar.realSpatialJet_spatialBounded line 561
  54. theorem OAI.SKFluctuations.Scalar.bddSmooth_of_uniform_real_chain line 567
  55. theorem OAI.SKFluctuations.Hierarchy.clockTest_scalar_spatialBounded line 588
  56. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_positiveJets_uniformBounded line 618
  57. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_positiveJets_bddSmooth line 638