LogarithmicForce.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The force produced by a logarithmic clock

This is the residual calculation in the slow-clock construction, with the linear viscous term separated from the quadratic material acceleration.

def OAI.ForcedComputation.slowVelocity line 20
def OAI.ForcedComputation.quadraticPhase line 23
def OAI.ForcedComputation.viscousPhase line 26
def OAI.ForcedComputation.slowForce line 29
theorem OAI.ForcedComputation.slowForce_eq_residual line 33

theorem OAI.ForcedComputation.slowForce_time_decay line 51

Source documentation

Uniform phase derivative bounds give exactly the slow-clock force estimate. The hypotheses refer to the original bounded periodic profiles, not to the force or to its desired decay.

theorem slowForce_time_decay (ν : ℝ) {V : Velocity}
    (hQ : ∀ x, ContDiff ℝ ∞ (quadraticPhase V x))
    (hD : ∀ x, ContDiff ℝ ∞ (viscousPhase V x))
    (hQB : UniformTimeBounds (quadraticPhase V))
    (hDB : UniformTimeBounds (viscousPhase V)) (n : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x t, 0 ≤ t →
      ‖iteratedDeriv n (fun s => slowForce ν V (s, x)) t‖ ≤
        C * (1 + t)⁻¹ ^ (1 + n) := by
…

Mentions: OAI.ForcedComputation.quadraticPhase, OAI.ForcedComputation.viscousPhase, OAI.ForcedComputation.UniformTimeBounds, OAI.ForcedComputation.slowForce