The linearly growing barrier of lem:aniso:comparison

The comparison argument for eq:aniso:comparison:equation is run against the barrier eq:aniso:comparison:barrier

Ψ_σ(x, τ) = M + σ (⟨x⟩ + K (τ - τ₀)), ⟨x⟩ = (1 + |x|²)^{1/2},

which grows linearly at infinity and is a supersolution of the drift-diffusion operator ∂_τ + B·∇ - Δ_X once the rate K dominates the drift bound and the number d of diffusive directions.

The Japanese bracket ⟨x⟩ is smooth on Vec m, bounds every coordinate, has gradient of length at most one, and has partial Laplacian at most d. Its derivatives are computed with the explicit iterated fderiv … (basisVec i), and the barrier facts are then restated with timeDeriv, gradPair, and partialLaplacian, so that they can be substituted into the distributional formulation of eq:aniso:comparison:equation directly.

The carrier of Vec m is the sup norm, for which the Cauchy-Schwarz bound on B·∇⟨x⟩ carries the dimensional factor √m; the rate is therefore K = √m Λ + d instead of the Λ + d of the printed proof, which measures the drift in the Euclidean norm. The inequality of eq:aniso:comparison:barrier is unaffected: only the size of K changes, and the comparison argument uses no upper bound on K.

The Japanese bracket

noncomputable def CIV.japaneseBracket (m : ℕ) (x : CKN.Vec m) : ℝ

The Japanese bracket ⟨x⟩ = (1 + |x|²)^{1/2} on Vec m, with |x| the Euclidean length of the coordinate vector x.

Equations

• CIV.japaneseBracket m x = √(1 + ∑ i : Fin m, x i ^ 2)

theorem CIV.one_le_japaneseBracket {m : ℕ} (x : CKN.Vec m) : 1 ≤ japaneseBracket m x

theorem CIV.japaneseBracket_pos {m : ℕ} (x : CKN.Vec m) : 0 < japaneseBracket m x

theorem CIV.japaneseBracket_ne_zero {m : ℕ} (x : CKN.Vec m) : japaneseBracket m x ≠ 0

theorem CIV.sq_japaneseBracket {m : ℕ} (x : CKN.Vec m) : japaneseBracket m x ^ 2 = 1 + ∑ i : Fin m, x i ^ 2

theorem CIV.sqrt_sum_sq_le_japaneseBracket {m : ℕ} (x : CKN.Vec m) : √(∑ i : Fin m, x i ^ 2) ≤ japaneseBracket m x

The Euclidean length of x is at most ⟨x⟩.

theorem CIV.abs_le_japaneseBracket {m : ℕ} (x : CKN.Vec m) (i : Fin m) : |x i| ≤ japaneseBracket m x

Every coordinate of x is bounded by ⟨x⟩.

theorem CIV.norm_le_japaneseBracket {m : ℕ} (x : CKN.Vec m) : ‖x‖ ≤ japaneseBracket m x

The sup norm of x is bounded by ⟨x⟩.

theorem CIV.contDiff_japaneseBracket {m : ℕ} : ContDiff ℝ (↑⊤) (japaneseBracket m)

theorem CIV.differentiable_japaneseBracket {m : ℕ} : Differentiable ℝ (japaneseBracket m)

First derivatives

theorem CIV.fderiv_japaneseBracket_apply {m : ℕ} (x v : CKN.Vec m) : (fderiv ℝ (japaneseBracket m) x) v = (∑ i : Fin m, x i * v i) / japaneseBracket m x

The gradient of ⟨x⟩ paired with a vector: ∇⟨x⟩ · v = (x · v) / ⟨x⟩.

theorem CIV.fderiv_japaneseBracket_basisVec {m : ℕ} (x : CKN.Vec m) (i : Fin m) : (fderiv ℝ (japaneseBracket m) x) (CKN.basisVec i) = x i / japaneseBracket m x

The coordinate partial derivative ∂_i⟨x⟩ = x_i / ⟨x⟩.

theorem CIV.sum_sq_fderiv_japaneseBracket_le_one {m : ℕ} (x : CKN.Vec m) : ∑ i : Fin m, (fderiv ℝ (japaneseBracket m) x) (CKN.basisVec i) ^ 2 ≤ 1

The gradient of ⟨x⟩ has Euclidean length at most one: ∑_i (∂_i⟨x⟩)² ≤ 1.

theorem CIV.abs_fderiv_japaneseBracket_apply_le {m : ℕ} (x v : CKN.Vec m) : |(fderiv ℝ (japaneseBracket m) x) v| ≤ √↑m * ‖v‖

Cauchy-Schwarz against the sup norm: |∇⟨x⟩ · v| ≤ √m ‖v‖.

Second derivatives

theorem CIV.differentiableAt_fderiv_japaneseBracket {m : ℕ} (x : CKN.Vec m) (i : Fin m) : DifferentiableAt ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (japaneseBracket m) y) (CKN.basisVec i)) x

theorem CIV.fderiv_fderiv_japaneseBracket {m : ℕ} (x : CKN.Vec m) (i : Fin m) : (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (japaneseBracket m) y) (CKN.basisVec i)) x) (CKN.basisVec i) = (japaneseBracket m x ^ 2 - x i ^ 2) / japaneseBracket m x ^ 3

The second coordinate derivative ∂_i∂_i⟨x⟩ = (⟨x⟩² - x_i²) / ⟨x⟩³.

theorem CIV.fderiv_fderiv_japaneseBracket_le_one {m : ℕ} (x : CKN.Vec m) (i : Fin m) : (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (japaneseBracket m) y) (CKN.basisVec i)) x) (CKN.basisVec i) ≤ 1

The second coordinate derivatives of ⟨x⟩ are bounded by one.

theorem CIV.sum_ite_fderiv_fderiv_japaneseBracket_le {m : ℕ} (d : ℕ) (x : CKN.Vec m) : (∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (japaneseBracket m) y) (CKN.basisVec i)) x) (CKN.basisVec i) else 0) ≤ ↑d

The partial Laplacian of ⟨x⟩ in the first d coordinates is at most d.

theorem CIV.fderiv_fderiv_japaneseBracket_nonneg {m : ℕ} (x : CKN.Vec m) (i : Fin m) : 0 ≤ (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (japaneseBracket m) y) (CKN.basisVec i)) x) (CKN.basisVec i)

The second coordinate derivatives of ⟨x⟩ are nonnegative: ⟨x⟩² - x_i² = 1 + ∑_{j ≠ i} x_j² ≥ 0, so the whole quotient by ⟨x⟩³ > 0 is nonnegative.

theorem CIV.sum_ite_fderiv_fderiv_japaneseBracket_nonneg {m : ℕ} (d : ℕ) (x : CKN.Vec m) : 0 ≤ ∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (japaneseBracket m) y) (CKN.basisVec i)) x) (CKN.basisVec i) else 0

The partial Laplacian of ⟨x⟩ in the first d coordinates is nonnegative: a sum of nonnegative terms.

The barrier Ψ_σ

noncomputable def CIV.barrier (m : ℕ) (M σ K τ₀ : ℝ) (z : CKN.Vec m × ℝ) : ℝ

The barrier eq:aniso:comparison:barrier: Ψ_σ(x, τ) = M + σ (⟨x⟩ + K (τ - τ₀)).

Equations

• CIV.barrier m M σ K τ₀ z = M + σ * (CIV.japaneseBracket m z.1 + K * (z.2 - τ₀))

noncomputable def CIV.barrierRate (m d : ℕ) (Λ : ℝ) : ℝ

The rate K = √m Λ + d of eq:aniso:comparison:barrier, for a drift bounded by Λ in the sup norm of Vec m and diffusion in the first d coordinates.

Equations

• CIV.barrierRate m d Λ = √↑m * Λ + ↑d

theorem CIV.barrierRate_nonneg (m d : ℕ) {Λ : ℝ} (hΛ : 0 ≤ Λ) : 0 ≤ barrierRate m d Λ

theorem CIV.contDiff_barrier {m : ℕ} (M σ K τ₀ : ℝ) : ContDiff ℝ (↑⊤) (barrier m M σ K τ₀)

theorem CIV.fderiv_barrier_time {m : ℕ} (M σ K τ₀ : ℝ) (x : CKN.Vec m) (t : ℝ) : (fderiv ℝ (fun (τ : ℝ) => barrier m M σ K τ₀ (x, τ)) t) 1 = σ * K

The time derivative of the barrier: ∂_τΨ_σ = σK.

theorem CIV.fderiv_barrier_spatial_apply {m : ℕ} (M σ K τ₀ τ : ℝ) (x v : CKN.Vec m) : (fderiv ℝ (fun (y : CKN.Vec m) => barrier m M σ K τ₀ (y, τ)) x) v = σ * ((∑ i : Fin m, x i * v i) / japaneseBracket m x)

The spatial gradient of the barrier paired with a vector: ∇Ψ_σ · v = σ (x · v) / ⟨x⟩.

theorem CIV.abs_fderiv_barrier_spatial_apply_le {m : ℕ} (M K τ₀ τ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (x v : CKN.Vec m) : |(fderiv ℝ (fun (y : CKN.Vec m) => barrier m M σ K τ₀ (y, τ)) x) v| ≤ σ * (√↑m * ‖v‖)

The drift term of the barrier is controlled by the sup norm of the drift: |B · ∇Ψ_σ| ≤ σ √m ‖B‖.

theorem CIV.fderiv_fderiv_barrier_spatial {m : ℕ} (M σ K τ₀ τ : ℝ) (x : CKN.Vec m) (i : Fin m) : (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (fun (w : CKN.Vec m) => barrier m M σ K τ₀ (w, τ)) y) (CKN.basisVec i)) x) (CKN.basisVec i) = σ * ((japaneseBracket m x ^ 2 - x i ^ 2) / japaneseBracket m x ^ 3)

The second spatial derivatives of the barrier: ∂_i∂_iΨ_σ = σ (⟨x⟩² - x_i²) / ⟨x⟩³.

theorem CIV.sum_ite_fderiv_fderiv_barrier_le {m : ℕ} (d : ℕ) (M K τ₀ τ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (x : CKN.Vec m) : (∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (fun (w : CKN.Vec m) => barrier m M σ K τ₀ (w, τ)) y) (CKN.basisVec i)) x) (CKN.basisVec i) else 0) ≤ σ * ↑d

The partial Laplacian of the barrier in the first d coordinates is at most σd.

theorem CIV.sum_ite_fderiv_fderiv_barrier_nonneg {m : ℕ} (d : ℕ) (M K τ₀ τ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (x : CKN.Vec m) : 0 ≤ ∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (fun (w : CKN.Vec m) => barrier m M σ K τ₀ (w, τ)) y) (CKN.basisVec i)) x) (CKN.basisVec i) else 0

The partial Laplacian of the barrier in the first d coordinates is nonnegative: the same term-by-term rescaling as sum_ite_fderiv_fderiv_barrier_le, against sum_ite_fderiv_fderiv_japaneseBracket_nonneg instead of the upper bound.

The barrier against the drift-diffusion operator

theorem CIV.timeDeriv_barrier {m : ℕ} (M σ K τ₀ : ℝ) (z : CKN.Vec m × ℝ) : timeDeriv m (barrier m M σ K τ₀) z = σ * K

∂_τΨ_σ = σK.

theorem CIV.gradPair_barrier {m : ℕ} (M σ K τ₀ : ℝ) (z : CKN.Vec m × ℝ) (v : CKN.Vec m) : gradPair m (barrier m M σ K τ₀) z v = σ * ((∑ i : Fin m, z.1 i * v i) / japaneseBracket m z.1)

∇Ψ_σ · v = σ (x · v) / ⟨x⟩.

theorem CIV.abs_gradPair_barrier_le {m : ℕ} (M K τ₀ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (z : CKN.Vec m × ℝ) (v : CKN.Vec m) : |gradPair m (barrier m M σ K τ₀) z v| ≤ σ * (√↑m * ‖v‖)

|∇Ψ_σ · v| ≤ σ √m ‖v‖ for the sup norm of Vec m.

theorem CIV.partialLaplacian_barrier_le {m : ℕ} (d : ℕ) (M K τ₀ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (z : CKN.Vec m × ℝ) : partialLaplacian m d (barrier m M σ K τ₀) z ≤ σ * ↑d

Δ_XΨ_σ ≤ σd.

theorem CIV.partialLaplacian_barrier_nonneg {m : ℕ} (d : ℕ) (M K τ₀ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (z : CKN.Vec m × ℝ) : 0 ≤ partialLaplacian m d (barrier m M σ K τ₀) z

Δ_XΨ_σ ≥ 0.

theorem CIV.barrier_supersolution {m : ℕ} (d : ℕ) (M τ₀ Λ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (B : CKN.Vec m × ℝ → CKN.Vec m) (z : CKN.Vec m × ℝ) (hB : ‖B z‖ ≤ Λ) : 0 ≤ timeDeriv m (barrier m M σ (barrierRate m d Λ) τ₀) z + gradPair m (barrier m M σ (barrierRate m d Λ) τ₀) z (B z) - partialLaplacian m d (barrier m M σ (barrierRate m d Λ) τ₀) z

The supersolution inequality of eq:aniso:comparison:barrier: with the rate K = √m Λ + d the barrier satisfies ∂_τΨ_σ + B·∇Ψ_σ - Δ_XΨ_σ ≥ 0 at every point where the drift is bounded by Λ.

theorem CIV.barrier_supersolution_slack_le {m : ℕ} (d : ℕ) (M τ₀ Λ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (B : CKN.Vec m × ℝ → CKN.Vec m) (z : CKN.Vec m × ℝ) (hB : ‖B z‖ ≤ Λ) : timeDeriv m (barrier m M σ (barrierRate m d Λ) τ₀) z + gradPair m (barrier m M σ (barrierRate m d Λ) τ₀) z (B z) - partialLaplacian m d (barrier m M σ (barrierRate m d Λ) τ₀) z ≤ σ * (2 * √↑m * Λ + ↑d)

An upper bound on the barrier's supersolution slack. barrier_supersolution bounds ∂_τΨ_σ + B·∇Ψ_σ - Δ_XΨ_σ from below by 0; this bounds the same quantity from above, by σ (2 √m Λ + d), from the exact value of ∂_τΨ_σ, the Cauchy–Schwarz bound on ∇Ψ_σ·B, and partialLaplacian_barrier_nonneg (dropping the Laplacian term, which can only decrease the slack).

theorem CIV.le_barrier {m : ℕ} (M K τ₀ τ : ℝ) {σ : ℝ} (x : CKN.Vec m) (hσ : 0 ≤ σ) (hK : 0 ≤ K) (hτ : τ₀ ≤ τ) : M + σ * ‖x‖ ≤ barrier m M σ K τ₀ (x, τ)

The barrier dominates M + σ‖x‖ after the initial time τ₀.