ResidualScaling.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Residual force under startup and changes of clock

The fields and differential operators are the concrete flat-coordinate ones already used by the shear realization. In particular, residual includes the convective term, which need not vanish for a spatial suspension.

def OAI.ForcedComputation.residual line 20
theorem OAI.ForcedComputation.derivative_smul line 24
theorem OAI.ForcedComputation.laplacian_smul line 30
theorem OAI.ForcedComputation.advection_smul line 39
theorem OAI.ForcedComputation.divergence_smul line 45
def OAI.ForcedComputation.rampVelocity line 49

theorem OAI.ForcedComputation.residual_ramp line 53

Source documentation

Formula (steady-force) in the eventually stationary forcing manuscript.

theorem residual_ramp (ν : ℝ) (α : ℝ → ℝ) (W : Space → Space)
    {t : ℝ} (hα : DifferentiableAt ℝ α t) (x : Space) :
    residual ν (rampVelocity α W) (t, x) =
      deriv α t • W x + α t ^ 2 • advection W x - ν • (α t • laplacian W x) := by
…

Mentions: OAI.ForcedComputation.residual, OAI.ForcedComputation.rampVelocity

theorem OAI.ForcedComputation.ramp_initial_zero line 63
theorem OAI.ForcedComputation.ramp_solenoidal line 67

theorem OAI.ForcedComputation.residual_ramp_of_eventually_one line 74

Source documentation

Once a startup ramp is locally one, its force is the stationary residual.

theorem residual_ramp_of_eventually_one (ν : ℝ) {α : ℝ → ℝ} (W : Space → Space)
    {t : ℝ} (hα : α =ᶠ[𝓝 t] fun _ => 1) (x : Space) :
    residual ν (rampVelocity α W) (t, x) = advection W x - ν • laplacian W x := by
…

Mentions: OAI.ForcedComputation.residual, OAI.ForcedComputation.rampVelocity

theorem OAI.ForcedComputation.residual_ramp_on_tail line 84
Source documentation
The endpoint of the stationary interval is included; differentiability forces the startup derivative to agree with the constant right-hand tail.
```
theorem residual_ramp_on_tail (ν : ℝ) {α : ℝ → ℝ} (W : Space → Space)
    (htail : ∀ s, 1 ≤ s → α s = 1) {t : ℝ} (ht : 1 ≤ t)
    (hα : DifferentiableAt ℝ α t) (x : Space) :
    residual ν (rampVelocity α W) (t, x) = advection W x - ν • laplacian W x := by
…
```
Mentions: OAI.ForcedComputation.residual, OAI.ForcedComputation.rampVelocity
def OAI.ForcedComputation.reparametrizedVelocity line 97

theorem OAI.ForcedComputation.residual_reparametrization line 101

Source documentation

The full clock-force formula, including convection and the clock acceleration.

theorem residual_reparametrization (ν : ℝ) {τ a : ℝ → ℝ} {V : Velocity}
    {t da : ℝ} (hτ : HasDerivAt τ (a t) t) (ha : HasDerivAt a da t)
    (x : Space) (hV : DifferentiableAt ℝ (fun s => V (s, x)) (τ t)) :
    residual ν (reparametrizedVelocity τ a V) (t, x) =
      da • V (τ t, x) - ν • (a t • laplacian (fun y => V (τ t, y)) x) +
        a t ^ 2 • (timeDerivative V (τ t) x + advection (fun y => V (τ t, y)) x) := by
…

Mentions: OAI.ForcedComputation.residual, OAI.ForcedComputation.reparametrizedVelocity

theorem OAI.ForcedComputation.reparametrized_initial_zero line 117
theorem OAI.ForcedComputation.reparametrized_solenoidal line 122