OAI/Probability/SKFluctuations/ClockDerivativeContinuous.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Clock Derivative Continuous.

  1. theorem OAI.SKFluctuations.Hierarchy.clockDerivative_continuous line 19
  2. theorem OAI.SKFluctuations.Hierarchy.clockDerivative_absBounded line 27
  3. theorem OAI.SKFluctuations.Hierarchy.clockDerivative_eq_generator line 35
  4. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockContinuation line 48
  5. theorem OAI.SKFluctuations.Hierarchy.clockTest_bddSmooth line 58
  6. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_regular line 64
  7. structure OAI.SKFluctuations.Hierarchy.HeatJet line 78
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.regular line 97
  9. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockContinuation_source_vector line 101
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.derivF_coord line 111
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.derivA_coord line 116
  12. def OAI.SKFluctuations.Hierarchy.HeatJet.evolve line 122
  13. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_time_F line 145
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_time_A line 153
  15. def OAI.SKFluctuations.Hierarchy.HeatJet.square line 169
  16. structure OAI.SKFluctuations.Hierarchy.HeatJetFamily line 196
  17. def OAI.SKFluctuations.Hierarchy.HeatJet.family line 212
  18. def OAI.SKFluctuations.Hierarchy.HeatJetFamily.square line 228
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuousP line 245
  20. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuousW line 250
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.boundedP line 257
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.boundedW line 264
  23. theorem OAI.SKFluctuations.Hierarchy.local_exponential_domination line 284
  24. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_tested_integral_local line 322
  25. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_tiltedMean_local line 356
  26. theorem OAI.SKFluctuations.Hierarchy.dynamic_testedPartition_continuous line 399
  27. theorem OAI.SKFluctuations.Hierarchy.dynamic_clockTest_continuous line 450
  28. theorem OAI.SKFluctuations.Hierarchy.dynamic_clockGradient_continuous line 471
  29. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_dynamic_clockTest line 494
  30. def OAI.SKFluctuations.Hierarchy.HeatJet.potentialRate line 555
  31. def OAI.SKFluctuations.Hierarchy.HeatJet.testRate line 557
  32. def OAI.SKFluctuations.Hierarchy.HeatJet.energy line 559
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smoothPotentialRate line 562
  34. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smoothTestRate line 565
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smoothEnergy line 568
  36. theorem OAI.SKFluctuations.Hierarchy.HeatJet.energy_nonneg line 572
  37. theorem OAI.SKFluctuations.Hierarchy.HeatJet.trace_eq_rate line 575
  38. theorem OAI.SKFluctuations.Hierarchy.HeatJet.square_trace line 583
  39. theorem OAI.SKFluctuations.Hierarchy.HeatJet.square_cancellation line 595
  40. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuousPotentialRate line 616
  41. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuousTestRate line 619
  42. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.boundedPotentialRate line 623
  43. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.boundedTestRate line 627