Documentation

LeanPool.AnomalousDiffusion.AVenhance.Statements.Construction.StreamVelLipschitz

Public statement.

theorem AVenhance.IsAdmissibleStream.vel_lipschitz {φ : ℝ → Homogenization.Vec 2 → ℝ} (h : IsAdmissibleStream φ) :
∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖streamVel φ t x - streamVel φ t y‖ ≤ L * ‖x - y‖

Uniform Lipschitz hypothesis of the flow, for the velocity of an admissible stream.