PlaneScalarInput.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth scalar advection-diffusion on the whole plane.

Ladyzhenskaya, Solonnikov and Ural'tseva, Linear and Quasi-linear Equations of Parabolic Type, AMS Translations of Mathematical Monographs 23 (1968), Chapter IV, Theorem 5.1, p.320; Cauchy problem (5.1)--(5.2), p.318 and bounded Hölder classes, p.319. We specialize to positive constant diffusion, smooth drift and source with common compact support on each finite slab, and zero initial data. Higher Hölder orders give smoothness up to the initial time from the right. The choice of Hölder order 3/2 also bounds spatial derivatives through order three on each finite slab.

def OAI.ForcedComputation.VelocityDetector.CompactPlaneCoefficients line 22
structure OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution line 26
def OAI.ForcedComputation.VelocityDetector.PlaneSpatialBounds line 38
Source documentation
Only the orders needed for local tail and H² estimates are retained. The bound may depend on the finite time interval and the coefficients.
```
def PlaneSpatialBounds (T : ℝ) (w : ℝ → Plane → ℝ) : Prop :=
…
```
def OAI.ForcedComputation.VelocityDetector.PlaneScalarExistence line 42
theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.slice_smooth line 49