OAI/Probability/SKFluctuations/ScalarArbitraryConcat.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Scalar Arbitrary Concat.

  1. theorem OAI.SKFluctuations.Hierarchy.floor_clock_error line 20
  2. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_concat line 32
  3. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_concat_grid_comparison line 83
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_concat line 120
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_remainder_bound line 181
  6. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_of_quadratic_remainder_on line 205
  7. theorem OAI.SKFluctuations.Hierarchy.second_derivative_remainder_on line 225
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_hasDerivAt line 253
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_congr_ae line 281
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_constant_Ioo line 293
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clock_terminal_deriv line 316
  12. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clock_terminal_taylor line 324
  13. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_clock_concat line 343
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_clock_concat line 353
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_zero line 397
  16. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_constant_Ioo line 410
  17. theorem OAI.SKFluctuations.Scalar.spatialJet_three_timePDE line 430
  18. theorem OAI.SKFluctuations.Scalar.spatialJet_four_timePDE line 449
  19. theorem OAI.SKFluctuations.Scalar.spatialJet_five_timePDE line 468
  20. theorem OAI.SKFluctuations.Scalar.realSpatialJet_time_transfer line 489
  21. def OAI.SKFluctuations.Scalar.invariantP line 506
  22. def OAI.SKFluctuations.Scalar.invariantQ line 507
  23. def OAI.SKFluctuations.Scalar.invariantR line 508
  24. def OAI.SKFluctuations.Scalar.invariantPD line 510
  25. def OAI.SKFluctuations.Scalar.invariantQD line 512
  26. def OAI.SKFluctuations.Scalar.invariantRD line 514
  27. def OAI.SKFluctuations.Scalar.invariantPx line 517
  28. def OAI.SKFluctuations.Scalar.invariantPxx line 518
  29. def OAI.SKFluctuations.Scalar.invariantQx line 519
  30. def OAI.SKFluctuations.Scalar.invariantQxx line 520
  31. def OAI.SKFluctuations.Scalar.invariantRx line 521
  32. def OAI.SKFluctuations.Scalar.invariantRxx line 523
  33. theorem OAI.SKFluctuations.Scalar.hasDerivAt_invariantP line 527
  34. theorem OAI.SKFluctuations.Scalar.hasDerivAt_invariantQ line 534
  35. theorem OAI.SKFluctuations.Scalar.hasDerivAt_invariantR line 543
  36. theorem OAI.SKFluctuations.Scalar.invariantPD_space line 552
  37. theorem OAI.SKFluctuations.Scalar.invariantQD_space line 556
  38. theorem OAI.SKFluctuations.Scalar.invariantRD_space line 560
  39. theorem OAI.SKFluctuations.Scalar.hasDerivAt_invariantPx line 564
  40. theorem OAI.SKFluctuations.Scalar.hasDerivAt_invariantQx line 573
  41. theorem OAI.SKFluctuations.Scalar.hasDerivAt_invariantRx line 582
  42. theorem OAI.SKFluctuations.Scalar.invariantP_time_algebra line 592
  43. theorem OAI.SKFluctuations.Scalar.invariantQ_time_algebra line 601
  44. theorem OAI.SKFluctuations.Scalar.invariantR_time_algebra line 611