The energy of (q_ε - Ψ_σ)_+ and the Grönwall step of lem:aniso:comparison

The comparison argument for eq:aniso:comparison:equation tests the mollified equation eq:aniso:comparison:mollified against the positive part

v_ε = (q_ε - Ψ_σ)_+

of the excess over the linearly growing barrier eq:aniso:comparison:barrier, and follows the energy

E(τ) = ∫ v_ε(x, τ)² dx.

This module supplies three groups of facts.

• Support and integrability. For τ ≥ τ₀ the function v_ε(·, τ) vanishes wherever ‖x‖ ≥ M_∞/σ, so it is a continuous function with compact support and E(τ) is an honest integral over closedBall 0 (M_∞/σ). At the initial time E(τ₀) = 0, because the barrier dominates M ≥ ‖q(·, τ₀)‖_{L^∞} there.

• The two right-hand terms of eq:aniso:comparison:positive:energy. The drift term ∫ (div B) v_ε² is bounded by Λ E(τ) whenever |div B| ≤ Λ, and the commutator term ∫ R_ε v_ε is bounded by ‖R_ε‖_{L²(B_{R_σ})} √(E(τ)) by Cauchy–Schwarz, the integral over ℝ^m reducing to one over closedBall 0 (M_∞/σ) by the support statement. The commutator of eq:aniso:comparison:mollified is square integrable on that ball, so the bound is not vacuous.

• Grönwall in integral form. If a continuous y ≥ 0 satisfies y(t) ≤ ∫_a^t (Λ y + 2 √y r) on [a, b], then y(t) ≤ (∫_a^b r²) exp((Λ + 1)(b - a)) there. The proof absorbs 2 √y r ≤ y + r² and then runs the integral-form Grönwall inequality le_mul_exp_of_le_primitive, which is proved by the fencing theorem applied to t ↦ (c + Λ ∫_a^t y) exp(-Λ(t - a)).

The integrated energy inequality itself — the passage from eq:aniso:comparison:mollified to eq:aniso:comparison:positive:energy — is not proved here; the last statement consumes it as a hypothesis in exactly the integrated form that the Grönwall step needs.

The excess over the barrier and its energy

noncomputable def CIV.comparisonPosPart (m : ℕ) (ε M σ K τ₀ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (z : CKN.Vec m × ℝ) : ℝ

The positive part v_ε = (q_ε - Ψ_σ)_+ of the excess of the mollified slice over the barrier eq:aniso:comparison:barrier.

Equations

• CIV.comparisonPosPart m ε M σ K τ₀ q z = max (CIV.mollifySlice m ε q z - CIV.barrier m M σ K τ₀ z) 0

noncomputable def CIV.comparisonEnergy (m : ℕ) (ε M σ K τ₀ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (τ : ℝ) : ℝ

The energy E(τ) = ∫ v_ε(x, τ)² dx of eq:aniso:comparison:positive:energy.

Equations

• CIV.comparisonEnergy m ε M σ K τ₀ q τ = ∫ (x : CKN.Vec m), CIV.comparisonPosPart m ε M σ K τ₀ q (x, τ) ^ 2

theorem CIV.comparisonPosPart_nonneg {m : ℕ} (ε M σ K τ₀ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (z : CKN.Vec m × ℝ) : 0 ≤ comparisonPosPart m ε M σ K τ₀ q z

theorem CIV.le_norm_of_notMem_closedBall {m : ℕ} {R : ℝ} {x : CKN.Vec m} (hx : x ∉ Metric.closedBall 0 R) : R ≤ ‖x‖

Outside a closed ball the norm is at least the radius.

Support and integrability

theorem CIV.comparisonPosPart_eq_zero_of_norm_ge {m : ℕ} {ε M σ K τ₀ τ Minf : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) (x : CKN.Vec m) (hx : Minf / σ ≤ ‖x‖) : comparisonPosPart m ε M σ K τ₀ q (x, τ) = 0

For τ ≥ τ₀ the excess vanishes off the ball of radius M_∞/σ: this is the statement that v_ε is compactly supported in x, uniformly on [τ₀, τ₊].

theorem CIV.continuous_comparisonPosPart {m : ℕ} {ε Minf : ℝ} (hε : 0 < ε) (M σ K τ₀ τ : ℝ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) : Continuous fun (x : CKN.Vec m) => comparisonPosPart m ε M σ K τ₀ q (x, τ)

The excess is continuous in the spatial variable: the mollified slice is smooth and the barrier is smooth.

theorem CIV.hasCompactSupport_comparisonPosPart {m : ℕ} {ε M σ K τ₀ τ Minf : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) : HasCompactSupport fun (x : CKN.Vec m) => comparisonPosPart m ε M σ K τ₀ q (x, τ)

theorem CIV.integrable_sq_comparisonPosPart {m : ℕ} {ε M σ K τ₀ τ Minf : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) : MeasureTheory.Integrable (fun (x : CKN.Vec m) => comparisonPosPart m ε M σ K τ₀ q (x, τ) ^ 2) MeasureTheory.volume

theorem CIV.comparisonEnergy_nonneg {m : ℕ} (ε M σ K τ₀ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (τ : ℝ) : 0 ≤ comparisonEnergy m ε M σ K τ₀ q τ

theorem CIV.comparisonEnergy_eq_setIntegral_closedBall {m : ℕ} {ε M σ K τ₀ τ Minf : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) : comparisonEnergy m ε M σ K τ₀ q τ = ∫ (x : CKN.Vec m) in Metric.closedBall 0 (Minf / σ), comparisonPosPart m ε M σ K τ₀ q (x, τ) ^ 2

The energy is an integral over the ball of radius M_∞/σ.

theorem CIV.comparisonEnergy_eq_zero_of_slice_le {m : ℕ} {ε M σ K τ₀ : ℝ} (hε : 0 < ε) (hσ : 0 ≤ σ) (hK : 0 ≤ K) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ₀)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ₀)| ≤ M) : comparisonEnergy m ε M σ K τ₀ q τ₀ = 0

The energy vanishes at the initial time, because the barrier dominates the bound M on the initial slice there.

Elementary inequalities behind the two right-hand terms

theorem CIV.two_mul_sqrt_mul_le_add_sq {u v : ℝ} (hu : 0 ≤ u) : 2 * √u * v ≤ u + v ^ 2

The absorption inequality 2 √u v ≤ u + v² for u ≥ 0.

theorem CIV.sq_integral_mul_le_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ) (hg : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ) : (∫ (x : α), f x * g x ∂μ) ^ 2 ≤ (∫ (x : α), f x ^ 2 ∂μ) * ∫ (x : α), g x ^ 2 ∂μ

Cauchy–Schwarz in squared form: (∫ f g)² ≤ (∫ f²)(∫ g²).

theorem CIV.integral_mul_le_sqrt_mul_sqrt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ) (hg : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ) : ∫ (x : α), f x * g x ∂μ ≤ √(∫ (x : α), f x ^ 2 ∂μ) * √(∫ (x : α), g x ^ 2 ∂μ)

Cauchy–Schwarz: ∫ f g ≤ ‖f‖_{L²} ‖g‖_{L²}.

theorem CIV.integral_bdd_mul_sq_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {w v : α → ℝ} {lam : ℝ} (hwm : MeasureTheory.AEStronglyMeasurable w μ) (hw : ∀ (x : α), |w x| ≤ lam) (hv : MeasureTheory.Integrable (fun (x : α) => v x ^ 2) μ) : ∫ (x : α), w x * v x ^ 2 ∂μ ≤ lam * ∫ (x : α), v x ^ 2 ∂μ

A weight bounded by Λ against a square: ∫ w v² ≤ Λ ∫ v².

The two right-hand terms of eq:aniso:comparison:positive:energy

theorem CIV.integral_bdd_mul_sq_comparisonPosPart_le {m : ℕ} {ε M σ K τ₀ τ Minf lam : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) {w : CKN.Vec m → ℝ} (hwm : MeasureTheory.AEStronglyMeasurable w MeasureTheory.volume) (hw : ∀ (x : CKN.Vec m), |w x| ≤ lam) : ∫ (x : CKN.Vec m), w x * comparisonPosPart m ε M σ K τ₀ q (x, τ) ^ 2 ≤ lam * comparisonEnergy m ε M σ K τ₀ q τ

The drift term of eq:aniso:comparison:positive:energy: a weight bounded by Λ, such as div B under eq:aniso:comparison:drift, contributes at most Λ E(τ).

theorem CIV.integrable_sq_diPernaLionsCommutator {m : ℕ} {ε Mq Rad : ℝ} {Λ : NNReal} (hε : 0 < ε) (hM : 0 ≤ Mq) {b : CKN.Vec m → CKN.Vec m} {divb g : CKN.Vec m → ℝ} (hlip : LipschitzWith Λ b) (hdivb : ∀ (y : CKN.Vec m), |divb y| ≤ ↑Λ) (hdivbm : MeasureTheory.AEStronglyMeasurable divb MeasureTheory.volume) (hg : ∀ (y : CKN.Vec m), |g y| ≤ Mq) (hgm : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : CKN.Vec m) => diPernaLionsCommutator m ε b divb g x ^ 2) (MeasureTheory.volume.restrict (Metric.closedBall 0 Rad))

The commutator R_ε of eq:aniso:comparison:mollified is square integrable on every closed ball: it is a.e. strongly measurable and uniformly bounded, and the ball has finite measure.

theorem CIV.integral_mul_comparisonPosPart_le {m : ℕ} {ε M σ K τ₀ τ Minf : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) {rf : CKN.Vec m → ℝ} (hrm : MeasureTheory.AEStronglyMeasurable rf (MeasureTheory.volume.restrict (Metric.closedBall 0 (Minf / σ)))) (hrsq : MeasureTheory.Integrable (fun (x : CKN.Vec m) => rf x ^ 2) (MeasureTheory.volume.restrict (Metric.closedBall 0 (Minf / σ)))) : ∫ (x : CKN.Vec m), rf x * comparisonPosPart m ε M σ K τ₀ q (x, τ) ≤ √(∫ (x : CKN.Vec m) in Metric.closedBall 0 (Minf / σ), rf x ^ 2) * √(comparisonEnergy m ε M σ K τ₀ q τ)

The commutator term of eq:aniso:comparison:positive:energy: since v_ε(·, τ) vanishes off closedBall 0 (M_∞/σ), Cauchy–Schwarz bounds ∫ R_ε v_ε by ‖R_ε‖_{L²(B_{R_σ})} √(E(τ)).

Grönwall in integral form

theorem CIV.le_mul_exp_of_le_primitive {y : ℝ → ℝ} {a b c lam : ℝ} (hab : a ≤ b) (hlam : 0 ≤ lam) (hc : 0 ≤ c) (hycont : ContinuousOn y (Set.Icc a b)) (hy : ∀ t ∈ Set.Icc a b, y t ≤ c + lam * ∫ (s : ℝ) in a..t, y s) (t : ℝ) : t ∈ Set.Icc a b → y t ≤ c * Real.exp (lam * (b - a))

Integral-form Grönwall inequality: a continuous y on [a, b] with y(t) ≤ c + Λ ∫_a^t y obeys y(t) ≤ c exp(Λ (b - a)).

The primitive F(t) = c + Λ ∫_a^t y is continuous on [a, b] and has right derivative Λ y(t) ≤ Λ F(t) there, so t ↦ F(t) exp(-Λ (t - a)) has nonpositive right derivative and the fencing theorem image_le_of_deriv_right_le_deriv_boundary bounds it by its value c at a.

theorem CIV.le_exp_mul_integral_sq_of_le_integral {y r : ℝ → ℝ} {a b lam : ℝ} (hab : a ≤ b) (hlam : 0 ≤ lam) (hynn : ∀ t ∈ Set.Icc a b, 0 ≤ y t) (hycont : ContinuousOn y (Set.Icc a b)) (hrcont : ContinuousOn r (Set.Icc a b)) (hineq : ∀ t ∈ Set.Icc a b, y t ≤ ∫ (s : ℝ) in a..t, lam * y s + 2 * √(y s) * r s) (t : ℝ) : t ∈ Set.Icc a b → y t ≤ (∫ (s : ℝ) in a..b, r s ^ 2) * Real.exp ((lam + 1) * (b - a))

The Grönwall step of lem:aniso:comparison, in the form the integrated energy inequality eq:aniso:comparison:positive:energy delivers it: from y(t) ≤ ∫_a^t (Λ y + 2 √y r) on [a, b] one gets y(t) ≤ (∫_a^b r²) exp((Λ + 1)(b - a)), so the supremum of y is controlled by the squared L² norm of r.

theorem CIV.comparisonEnergy_le_exp_mul_integral_sq {m : ℕ} {ε M σ K τ₀ tplus lam : ℝ} {q : CKN.Vec m × ℝ → ℝ} {r : ℝ → ℝ} (hab : τ₀ ≤ tplus) (hlam : 0 ≤ lam) (hcont : ContinuousOn (comparisonEnergy m ε M σ K τ₀ q) (Set.Icc τ₀ tplus)) (hrcont : ContinuousOn r (Set.Icc τ₀ tplus)) (hineq : ∀ τ ∈ Set.Icc τ₀ tplus, comparisonEnergy m ε M σ K τ₀ q τ ≤ ∫ (s : ℝ) in τ₀..τ, lam * comparisonEnergy m ε M σ K τ₀ q s + 2 * √(comparisonEnergy m ε M σ K τ₀ q s) * r s) (τ : ℝ) : τ ∈ Set.Icc τ₀ tplus → comparisonEnergy m ε M σ K τ₀ q τ ≤ (∫ (s : ℝ) in τ₀..tplus, r s ^ 2) * Real.exp ((lam + 1) * (tplus - τ₀))

The Grönwall conclusion for the energy of eq:aniso:comparison:positive:energy: once the integrated energy inequality is available on [τ₀, τ₊], the energy is bounded there by the squared L² norm of the commutator times a constant depending only on Λ and τ₊ - τ₀.