LinearExitDatum #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The linear datum of the exit-time problem #

The exit-time comparison of Section 5.2 writes the constant right-hand side 1 as the divergence of the linear vector field g(x) = x_1 e_1, so that the exit-time equation becomes an instance of the localized Dirichlet problem -∇·a∇w = ∇·g of Section 5.1, whose homogenization is the injection estimate.

Two facts are needed about that datum: its 1/2-Hölder seminorm on a cube of side 3^n is at most 3^{n/2}, so that the injection estimate's right-hand side is C ε 3^{n/2} · 3^{n/2} = C ε 3^n; and its weak form is the constant forcing, ∫ a∇w·∇φ = ∫ φ, which is the equation -∇·a∇w = 1.

The sign #

IsDirichletSolutionAt renders -∇·a∇u = ∇·g as ∫ a∇u·∇φ = -∫ g·∇φ. With g(x) = x_1 e_1 the right side is -∫ x_1 ∂_1φ = +∫ φ, one integration by parts against a zero-trace test function; so the datum g carries the positive constant forcing and the solution is the (nonnegative) exit-time profile, not its negative.

Main definitions #

linearAxisDatum i — the field x ↦ x_i e_i.

Main results #

vecFieldDiv_linearAxisDatum — ∇·g = 1.
holderSeminormOn_linearAxisDatum_le — [g]_{C^{0,1/2}(y+□_n)} ≤ 3^{n/2}.
isDirichletSolutionAt_linearAxisDatum_iff — the weak form of the datum is the constant forcing ∫ a∇u·∇φ = ∫ φ.

References #

ABK26, the exit-time comparison of Section 5.2.

1. The field and its divergence #

source

def Algsuperdiff.Section5.Support.linearAxisDatum {d : ℕ} (i : Fin d) :

HCPolySupport.Vec d → HCPolySupport.Vec d

The linear datum g(x) = x_i e_i, whose divergence is the constant 1.

Equations

Algsuperdiff.Section5.Support.linearAxisDatum i x = x i • HCPolySupport.basisVec i

Instances For

source

theorem Algsuperdiff.Section5.Support.contDiff_linearAxisDatum_coord {d : ℕ} (i j : Fin d) :

ContDiff ℝ 1 fun (z : HCPolySupport.Vec d) => linearAxisDatum i z j

Each component of the linear datum is C¹.

source

theorem Algsuperdiff.Section5.Support.vecFieldDiv_linearAxisDatum {d : ℕ} (i : Fin d) (x : HCPolySupport.Vec d) :

vecFieldDiv (linearAxisDatum i) x = 1

∇·g = 1 for the linear datum g(x) = x_i e_i.

2. The Hölder seminorm of the linear datum #

source

theorem Algsuperdiff.Section5.Support.holderSeminormBoundOn_linearAxisDatum {d : ℕ} (i : Fin d) (y : HCPolySupport.Vec d) (n : ℤ) :

Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) (Real.rpow 3 (↑n / 2)) (linearAxisDatum i)

The 1/2-Hölder bound for the linear datum on a cube of side 3^n. The dimensional constant is 1: the increment of g is one coordinate increment, which the supremum norm dominates.

source