OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/StartupClock.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A startup ramp has an onto accumulated clock

This supplies the time-change argument in the eventually stationary forcing construction. Nonnegativity controls the initial interval; the constant tail ensures that every finite computational time is reached.

  1. def OAI.ForcedComputation.accumulatedClock line 21
  2. theorem OAI.ForcedComputation.accumulatedClock_zero line 23
  3. theorem OAI.ForcedComputation.accumulatedClock_hasDerivAt line 26
  4. theorem OAI.ForcedComputation.accumulatedClock_nonneg line 31
  5. theorem OAI.ForcedComputation.accumulatedClock_tail line 36
  6. theorem OAI.ForcedComputation.accumulatedClock_onto line 51
  7. def OAI.ForcedComputation.startupRamp line 69

    Source documentation

    A completely specified fixed startup, zero until time 1/2 and one from time 1.

    def startupRamp (t : ℝ) : ℝ := Real.smoothTransition (2 * t - 1)
  8. theorem OAI.ForcedComputation.startupRamp_smooth line 71
  9. theorem OAI.ForcedComputation.startupRamp_zero line 74
  10. theorem OAI.ForcedComputation.startupRamp_nonneg line 78
  11. theorem OAI.ForcedComputation.startupRamp_tail line 81
  12. theorem OAI.ForcedComputation.startupClock_onto line 85