ComparatorComparison

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

The weak comparison principle for the constant-coefficient problem on a cube

The homogenized exit-time profile solves -σ Δ w = 1 on y + □_n with zero boundary values. Every lower bound for it is obtained from a barrier: a zero-trace function v with -σ Δ v ≤ 1 weakly lies below w. This module proves that comparison, in the form used twice by the exit-time estimate — once with the barrier v = 0, which gives w ≥ 0, and once with a bump barrier, which gives the lower bound on the inner cube.

The argument is the standard energy argument: the positive part (v - w)₊ of the difference has zero trace, its gradient is 1_{v>w} ∇(v - w), and testing the two relations against it gives σ ∫ |∇(v-w)₊|² ≤ 0; the Poincaré inequality on H¹₀ then forces (v - w)₊ = 0.

Main results

• ae_le_of_constantForcingSubsolution — the comparison.
• le_of_ae_le_of_continuousOn — an almost-everywhere inequality between two functions continuous on an open set is a pointwise inequality.

References

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

1. From an almost-everywhere inequality to a pointwise one

theorem Algsuperdiff.Section5.Support.le_of_ae_le_of_continuousOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {f g : HCPolySupport.Vec d → ℝ} (hae : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, f x ≤ g x) (hf : ContinuousOn f U) (hg : ContinuousOn g U) (x : HCPolySupport.Vec d) : x ∈ U → f x ≤ g x

On an open set, an almost-everywhere inequality between functions continuous there is a pointwise inequality. The set where it fails is open and null, hence empty.

2. The comparison

theorem Algsuperdiff.Section5.Support.ae_le_of_constantForcingSubsolution {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (hd : 0 < d) {sig : ℝ} (hsig : 0 < sig) {w : HCPolySupport.H1Function (cubeSetAt y n)} (hw0 : ∃ (w0 : HCPolySupport.H10Function (cubeSetAt y n)), (∀ (x : HCPolySupport.Vec d), w.toFun x = w0.toFun x) ∧ ∀ (x : HCPolySupport.Vec d), w.grad x = w0.grad x) (hw : ∀ (phi : HCPolySupport.H10Function (cubeSetAt y n)), sig * ∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, HCPolySupport.vecDot (w.grad x) (phi.grad x) = ∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, phi.toFun x) (v : HCPolySupport.H10Function (cubeSetAt y n)) (hv : ∀ (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) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (cubeSetAt y n), v.toFun x ≤ w.toFun x

The weak comparison principle for -σ Δ · = 1 on the cube y + □_n. A zero-trace subsolution lies below the zero-trace solution almost everywhere.

hw0 records that w has zero trace, hw that it solves the equation, and hv that v is a subsolution: both relations are stated in the constant-forcing weak form σ ∫ ∇u·∇φ = ∫ φ in which the linear datum puts the problem.