ExitMeanValueIdentificationLevel

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

The harmonic part of a cube resolvent at a finite exhaustion level

Fix two exhaustion cubes V ⊆ W and a positive shift. The Dirichlet resolvent of W applied to a bounded measurable datum is an honest H¹ function of W — this is the level-W solution of ExitTimePDEIdentification.lean, with its value function replaced by the exact continuous representative — and it solves -div (a grad psi) = f - mu psi weakly on W, hence also weakly on V.

Subtracting the Green potential on V of the same residual f - mu psi, which is the zero-trace solution of -div (a grad w) = f - mu psi on V, leaves a function that is weakly a-harmonic on V and differs from psi by that zero-trace function. That is the level-W harmonic part.

No limit and no compactness argument is used: at a finite level the resolvent is a zero-trace Sobolev function of the larger cube by construction, and restriction of the weak equation to an open subset is the zero-extension of test functions.

The residual of a cube resolvent

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeLevelResidual {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : HCPolySupport.Vec d → ℝ

The residual of the Dirichlet resolvent of an exhaustion cube: the datum less the shift times the resolvent.

Equations

• A.cubeLevelResidual m mu hf hfD y = f y - ↑mu * A.analyticCubeResolvent mu f hf hfD m y

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_cubeLevelResidual {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : Measurable (A.cubeLevelResidual m mu hf hfD)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_cubeLevelResidual_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (y : HCPolySupport.Vec d) : |A.cubeLevelResidual m mu hf hfD y| ≤ 2 * D

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeLevelResidualBound_nonneg {D : ℝ} (hD : 0 ≤ D) : 0 ≤ 2 * D

The exact H¹ representative of a cube resolvent

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_cubeResolventH1 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ∃ (z : HCPolySupport.H1Function (wholeSpaceCube d m)), z.toFun = A.analyticCubeResolvent mu f hf hfD m ∧ IsScalarForcedWeakSolution A.a (wholeSpaceCube d m) (A.cubeLevelResidual m mu hf hfD) z

The Dirichlet resolvent of an exhaustion cube is an H¹ function of that cube whose value function is the continuous representative, and it solves the shifted equation with the residual as forcing.

The level harmonic part