ExitTimeBarrier

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

A barrier from below for the homogenized exit-time problem

The homogenized exit time on y + □_n is bounded below on the inner cube y + □_{n-1} by comparison with a barrier: a smooth bump supported strictly inside y + □_n, equal to a constant A on a ball containing the inner cube, and scaled so that its Laplacian is small enough that it is a subsolution of -σ Δ · = 1.

The scaling is the only quantitative point. A fixed bump η on the unit scale has a bounded Laplacian, |Δη| ≤ K(d) on the ball of radius 1/2; the rescaled bump x ↦ A η(3^{-n}(x - y)) therefore has |Δ| ≤ A 3^{-2n} K, so the choice A = 3^{2n} / (σ K) makes -σ Δ at most 1 — and the barrier reaches the height A = 3^{2n}/(σK), which is the exit-time scale up to the constant K.

The ambient norm on Vec d is the supremum norm, so its balls are the cubes: cubeSetAt y n = Metric.ball y (3^n/2). A single bump with rIn = 1/6 and rOut = 1/3 therefore covers the whole inner cube and is supported strictly inside the cube, with no dependence on the dimension in the geometry.

Main definitions

• referenceBump d — the unit-scale bump, 1 on the ball of radius 1/6, supported in the ball of radius 1/3.
• exitTimeBarrier y n A — the rescaled barrier of height A on y + □_n.

Main results

• exists_exitTimeBarrier — the barrier as a zero-trace Sobolev function, with its height on the inner cube and its subsolution property.

References

• ABK26, the exit-time comparison of Section 5.2.

1. The reference bump and its Laplacian

noncomputable def Algsuperdiff.Section5.Support.referenceBump (d : ℕ) : ContDiffBump 0

The unit-scale bump: equal to 1 on the ball of radius 1/6 and supported in the ball of radius 1/3.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Support.contDiff_referenceBump (d : ℕ) : ContDiff ℝ ↑⊤ fun (z : HCPolySupport.Vec d) => ↑(referenceBump d) z

theorem Algsuperdiff.Section5.Support.contDiff_euclideanCoordDeriv_referenceBump (d : ℕ) (i : Fin d) : ContDiff ℝ 1 fun (z : HCPolySupport.Vec d) => HCPolySupport.euclideanCoordDeriv i (fun (w : HCPolySupport.Vec d) => ↑(referenceBump d) w) z

noncomputable def Algsuperdiff.Section5.Support.bumpLaplacian (d : ℕ) : HCPolySupport.Vec d → ℝ

The Laplacian of the reference bump.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Support.bumpLaplacian_eq (d : ℕ) (t : HCPolySupport.Vec d) : bumpLaplacian d t = ∑ i : Fin d, (fderiv ℝ (fun (w : HCPolySupport.Vec d) => HCPolySupport.euclideanCoordDeriv i (fun (s : HCPolySupport.Vec d) => ↑(referenceBump d) s) w) t) (HCPolySupport.basisVec i)

theorem Algsuperdiff.Section5.Support.continuous_bumpLaplacian (d : ℕ) : Continuous (bumpLaplacian d)

theorem Algsuperdiff.Section5.Support.exists_bumpLaplacian_bound (d : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (t : HCPolySupport.Vec d), ‖t‖ ≤ 1 / 2 → |bumpLaplacian d t| ≤ K

The Laplacian of the reference bump is bounded on the ball of radius 1/2, the range of the rescaled argument over the cube.

2. The rescaled barrier

noncomputable def Algsuperdiff.Section5.Support.exitTimeBarrier {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (A : ℝ) : HCPolySupport.Vec d → ℝ

The barrier of height A on y + □_n.

Equations

• Algsuperdiff.Section5.Support.exitTimeBarrier y n A z = A * ↑(Algsuperdiff.Section5.Support.referenceBump d) ((3 ^ n)⁻¹ • (z - y))

3. The barrier as a zero-trace Sobolev function

theorem Algsuperdiff.Section5.Support.exists_exitTimeBarrier (d : ℕ) (y : HCPolySupport.Vec d) (n : ℤ) {sig : ℝ} (hsig : 0 < sig) {K : ℝ} (hK : 0 < K) (hKbd : ∀ (t : HCPolySupport.Vec d), ‖t‖ ≤ 1 / 2 → |bumpLaplacian d t| ≤ K) : ∃ (v : HCPolySupport.H10Function (cubeSetAt y n)), Continuous v.toFun ∧ (∀ x ∈ cubeSetAt y (n - 1), v.toFun x = (3 ^ n) ^ 2 / (sig * K)) ∧ ∀ (phi : HCPolySupport.H10Function (cubeSetAt y n)), (∀ (x : HCPolySupport.Vec d), 0 ≤ phi.toFun x) → sig * ∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, HCPolySupport.vecDot (v.grad x) (phi.grad x) ≤ ∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, phi.toFun x

The rescaled barrier, as a zero-trace Sobolev function on y + □_n, with its height on the inner cube and its subsolution property.