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

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Derivative bounds for the logarithmic clock

This is the analytic calculation in Lemma bcs:clock of Scalar Potentials and Slow Clocks for Forced Fluid Computation. It proves the decay of every time derivative, rather than assuming decay of the reparametrized field.

  1. def OAI.ForcedComputation.logarithmicProfile line 22
  2. def OAI.ForcedComputation.phaseDerivative line 25
  3. def OAI.ForcedComputation.phaseIter line 28
  4. theorem OAI.ForcedComputation.logarithmicProfile_contDiffAt line 31
  5. theorem OAI.ForcedComputation.logarithmicProfile_hasDerivAt line 39
  6. theorem OAI.ForcedComputation.phaseDerivative_smooth line 62
  7. theorem OAI.ForcedComputation.phaseIter_smooth line 66
  8. theorem OAI.ForcedComputation.iteratedDeriv_logarithmicProfile line 72
  9. def OAI.ForcedComputation.HasBoundedTimeDerivatives line 88
  10. theorem OAI.ForcedComputation.iteratedDeriv_phaseDerivative line 91
  11. theorem OAI.ForcedComputation.phaseDerivative_bounded line 103
  12. theorem OAI.ForcedComputation.phaseIter_bounded line 118
  13. theorem OAI.ForcedComputation.logarithmicProfile_decay line 126

    Source documentation

    Each time derivative gains a full inverse power of physical time.

    theorem logarithmicProfile_decay (r n : ℕ) {A : ℝ → E}
    (hA : ContDiff ℝ ∞ A) (hbound : HasBoundedTimeDerivatives A) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ t : ℝ, 0 ≤ t →
      ‖iteratedDeriv n (logarithmicProfile r A) t‖ ≤ C * (1 + t)⁻¹ ^ (r + n) := by
…

    Mentions: OAI.ForcedComputation.HasBoundedTimeDerivatives, OAI.ForcedComputation.logarithmicProfile

  14. def OAI.ForcedComputation.UniformTimeBounds line 141

    Source documentation

    Bounds uniform in the spatial point (or a spatial derivative index).

    def UniformTimeBounds (A : ι → ℝ → E) : Prop :=
…
  15. theorem OAI.ForcedComputation.phaseDerivative_uniform line 144
  16. theorem OAI.ForcedComputation.phaseIter_uniform line 160
  17. theorem OAI.ForcedComputation.logarithmicProfile_uniform_decay line 168