ExcessiveCubeRemainder

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

The cube remainder of the whole-space barrier

On an exhaustion cube containing the part domain, the difference between the cube resolvent of the observable and the zero extension of the part solution is a nonnegative weak supersolution of the shifted equation with zero right-hand side. This is the second analytic step of the comparison: the resolvent solves the equation, the zero extension is a subsolution, and their difference is therefore a supersolution.

The truncated barriers increase along the exhaustion and converge pointwise to the whole-space barrier, which is therefore nonnegative everywhere. The truncated barrier vanishes off its own cube, because the observable and the part solution both vanish there.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.bound_nonneg {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : 0 ≤ P.D

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.measurable_utilde {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : Measurable P.utilde

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.abs_utilde_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (x : HCPolySupport.Vec d) : |P.utilde x| ≤ P.D / ↑P.lam

The continuous part solution obeys the sharp resolvent bound.

noncomputable def DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeBarrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) : HCPolySupport.Vec d → ℝ

The barrier truncated at one exhaustion cube.

Equations

• P.cubeBarrier m x = A.analyticCubeResolvent P.lam P.f ⋯ ⋯ m x - P.utilde x

noncomputable def DivergenceFormProcess.Form.WholeSpaceBarrierData.barrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : HCPolySupport.Vec d → ℝ

The whole-space barrier.

Equations

• P.barrier x = (A.analyticMinimalResolvent P.lam P.f ⋯ ⋯ x).toReal - P.utilde x

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.measurable_cubeBarrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) : Measurable (P.cubeBarrier m)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.measurable_barrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : Measurable P.barrier

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.abs_cubeBarrier_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (x : HCPolySupport.Vec d) : |P.cubeBarrier m x| ≤ 2 * (P.D / ↑P.lam)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.abs_barrier_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (x : HCPolySupport.Vec d) : |P.barrier x| ≤ 2 * (P.D / ↑P.lam)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.continuousOn_cubeBarrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) : ContinuousOn (P.cubeBarrier m) (wholeSpaceCube d m)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeBarrier_of_notMem {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) {x : HCPolySupport.Vec d} (hx : x ∉ wholeSpaceCube d m) : P.cubeBarrier m x = 0

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.utilde_ae_cube {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) : P.utilde =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] ↑↑(ZeroTraceSobolev.toL2 (P.cubeZeroExtension m hVU))

On an exhaustion cube containing the part domain, the continuous zero extension represents the L² zero extension.

noncomputable def DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeRemainder {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) : ZeroTraceSobolev (wholeSpaceCube d m)

The remainder on one exhaustion cube: the cube resolvent minus the zero extension of the part solution.

Equations

• P.cubeRemainder m hVU = (DivergenceFormProcess.Form.alphaShiftedSolution A.a ⋯ ⋯ ⋯) (DivergenceFormProcess.Form.boundedMeasurableToScalarL2 ⋯ ⋯ ⋯) - P.cubeZeroExtension m hVU

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeRemainder_nonneg_ae {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d m), 0 ≤ ↑↑(ZeroTraceSobolev.toL2 (P.cubeRemainder m hVU)) x

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeBarrier_ae {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) : P.cubeBarrier m =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] ↑↑(ZeroTraceSobolev.toL2 (P.cubeRemainder m hVU))

The truncated barrier represents the cube remainder.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeBarrier_nonneg {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (hVU : P.V ⊆ wholeSpaceCube d m) (x : HCPolySupport.Vec d) : 0 ≤ P.cubeBarrier m x

The truncated barrier is nonnegative everywhere.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeBarrier_mono {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) {m n : ℕ} (hmn : m ≤ n) (x : HCPolySupport.Vec d) : P.cubeBarrier m x ≤ P.cubeBarrier n x

The truncated barriers increase along the exhaustion.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.tendsto_cubeBarrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (x : HCPolySupport.Vec d) : Filter.Tendsto (fun (m : ℕ) => P.cubeBarrier m x) Filter.atTop (nhds (P.barrier x))

The truncated barriers converge to the whole-space barrier.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.cubeBarrier_le_barrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (m : ℕ) (x : HCPolySupport.Vec d) : P.cubeBarrier m x ≤ P.barrier x

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.barrier_nonneg {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (x : HCPolySupport.Vec d) : 0 ≤ P.barrier x

The whole-space barrier is nonnegative.