ExcessiveCubeMaximum

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

The pointwise maximum principle for the cube remainder

The cube remainder is a nonnegative weak supersolution of the shifted equation with zero right-hand side, so the almost-everywhere maximum principle of the part-domain layer applies to it. Both sides of that inequality are continuous on the cube, so it holds at every point of the cube; off the cube both sides vanish, so it holds everywhere.

This is the lam-excessiveness inequality of the truncated barrier, in the exact shape consumed by the exponential comparison of the process layer.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.boundedMeasurableToScalarL2_cubeBarrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) : boundedMeasurableToScalarL2 ⋯ ⋯ ⋯ = ZeroTraceSobolev.toL2 (P.cubeRemainder m hVU)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.mul_analyticCubeResolvent_cubeBarrier_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : ↑P.lam < ↑mu) (x : HCPolySupport.Vec d) : ↑mu * A.analyticCubeResolvent mu (P.cubeBarrier m) ⋯ ⋯ m x ≤ ↑mu / (↑mu - ↑P.lam) * P.cubeBarrier m x

The pointwise weak maximum principle on one exhaustion cube.