The spatial energy inequality at one time slice

This is the spatial half of eq:aniso:comparison:positive:energy. Fix a time s at which the slice q(·, s) is measurable and essentially bounded, and the drift slice B(·, s) is bounded, Lipschitz, with bounded weak divergence. Let w = q_ε(·, s) - Ψ_σ(·, s) be the excess of the mollified slice over the barrier eq:aniso:comparison:barrier, G the comparison profile and H the right side of eq:aniso:comparison:mollified. Then

∫ G'(w) (H - ∂_τΨ_σ) ≤ Λ ∫ G(w) + ∫ G'(w) |R_ε|.

The three contributions are those of the manuscript: the barrier is a supersolution, so H - ∂_τΨ_σ ≤ Δ_X w - B·∇w + R_ε pointwise; the diffusion term ∫ G'(w) Δ_X w = -∫ G''(w)|∇_X w|² is nonpositive (integration by parts twice, G convex); the transport term -∫ G'(w) B·∇w = ∫ (div B) G(w) is at most Λ ∫ G(w) by the weak divergence identity applied to the test function G ∘ w, which is smooth with compact support since w < 0 off a ball.

theorem CIV.fderiv_comp_real_apply {m : ℕ} {g : ℝ → ℝ} {f : CKN.Vec m → ℝ} {x : CKN.Vec m} (hg : Differentiable ℝ g) (hf : DifferentiableAt ℝ f x) (v : CKN.Vec m) : (fderiv ℝ (fun (y : CKN.Vec m) => g (f y)) x) v = deriv g (f x) * (fderiv ℝ f x) v

Chain rule for a scalar function composed with a function on Vec m.

theorem CIV.mollifySlice_sub_barrier_neg {m : ℕ} {ε : ℝ} (hε : 0 < ε) {q : CKN.Vec m × ℝ → ℝ} {s Mq M σ K τ₀ : ℝ} (hσ : 0 < σ) (hM : 0 ≤ M) (hK : 0 ≤ K) (hτs : τ₀ ≤ s) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, s)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, s)| ≤ Mq) {x : CKN.Vec m} (hx : x ∉ Metric.closedBall 0 (Mq / σ)) : mollifySlice m ε q (x, s) - barrier m M σ K τ₀ (x, s) < 0

The excess of the mollified slice over the barrier is negative off the ball of radius Mq / σ, once the slice is bounded by Mq and τ₀ ≤ s.

theorem CIV.integral_smoothTransition_mul_mollifiedRHS_le {m : ℕ} (d : ℕ) {ε σ M Mq τ₀ s : ℝ} {Λ : NNReal} (hε : 0 < ε) (hσ : 0 < σ) (hM : 0 ≤ M) (hMq : 0 ≤ Mq) (hτs : τ₀ ≤ s) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, s)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, s)| ≤ Mq) (hBb : ∀ (x : CKN.Vec m), ‖B (x, s)‖ ≤ ↑Λ) (hBlip : LipschitzWith Λ fun (x : CKN.Vec m) => B (x, s)) (hdiv : ∀ (x : CKN.Vec m), |divB (x, s)| ≤ ↑Λ) (hdivm : MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Vec m) => divB (x, s)) MeasureTheory.volume) (hweak : ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Vec m), divB (x, s) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, B (x, s) i * (fderiv ℝ ψ x) (CKN.basisVec i)) : ∫ (x : CKN.Vec m), (mollifySlice m ε q (x, s) - barrier m M σ (barrierRate m d ↑Λ) τ₀ (x, s)).smoothTransition * (mollifiedRHS m d ε B divB q x s - σ * barrierRate m d ↑Λ) ≤ (↑Λ * ∫ (x : CKN.Vec m), comparisonProfile (mollifySlice m ε q (x, s) - barrier m M σ (barrierRate m d ↑Λ) τ₀ (x, s))) + ∫ (x : CKN.Vec m), (mollifySlice m ε q (x, s) - barrier m M σ (barrierRate m d ↑Λ) τ₀ (x, s)).smoothTransition * |diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, s)) (fun (y : CKN.Vec m) => divB (y, s)) (fun (y : CKN.Vec m) => q (y, s)) x|

Spatial energy inequality at one time slice.