Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.FullTheorem.Contracts.LemmaU

Lemma U (uniform time-Hölder bound in L²), proved #

lemmaU_contract discharges LemmaUContract: for a bounded, measurable, periodic, divergence-free drift and 0 < κ ≤ 1, every weak solution with H¹ datum satisfies ‖θ(t) − θ(s)‖ ≤ 40 (1 + B) κ^{-1/2} |t − s|^{1/4} ‖θ₀‖_{H¹}.