Reparametrization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Material trajectories under an onto clock

The change of clock used in §6 of Universal Computation with Eventually Stationary Navier–Stokes Forcing and in Scalar Potentials and Slow Clocks for Forced Fluid Computation. These lemmas concern the actual ODE and observation event; no computation/flow correspondence is postulated here.

def OAI.ForcedComputation.Reaches line 24
Source documentation
The nonnegative-time particle observation used in the manuscripts.
```
def Reaches (X : ℝ → E) (O : Set E) : Prop :=
…
```
def OAI.ForcedComputation.OntoClock line 28
Source documentation
A clock visits every nonnegative internal time and never visits a negative one.
```
def OntoClock (τ : ℝ → ℝ) : Prop :=
…
```
theorem OAI.ForcedComputation.reaches_comp_iff line 31

theorem OAI.ForcedComputation.trajectory_reparametrization line 41

Source documentation

Chain rule for the material ODE, including the initial condition.

theorem trajectory_reparametrization [NormedAddCommGroup E] [NormedSpace ℝ E]
    {V : ℝ → E → E} {X : ℝ → E}
    {τ a : ℝ → ℝ} {x₀ : E}
    (hX₀ : X 0 = x₀) (hτ₀ : τ 0 = 0)
    (hX : ∀ s, 0 ≤ s → HasDerivAt X (V s (X s)) s)
    (hτ : ∀ t, 0 ≤ t → HasDerivAt τ (a t) t)
    (hnonneg : ∀ t, 0 ≤ t → 0 ≤ τ t) :
    (X ∘ τ) 0 = x₀ ∧
      ∀ t, 0 ≤ t → HasDerivAt (X ∘ τ)
        (a t • V (τ t) ((X ∘ τ) t)) t := by
…

def OAI.ForcedComputation.logClock line 58
Source documentation
The logarithmic slowdown traverses infinitely many periods.
```
noncomputable def logClock (t : ℝ) : ℝ := Real.log (1 + t)
```
theorem OAI.ForcedComputation.logClock_onto line 60
theorem OAI.ForcedComputation.logClock_hasDerivAt line 68
theorem OAI.ForcedComputation.logClock_reaches_iff line 74