PartWholeHarmonic

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

The whole-space resolvent and its harmonic part on a bounded part domain

The whole-space resolvent psi = R_mu f is an H¹ function of every exhaustion cube and solves -div (a grad psi) = f - mu psi weakly there.

A bounded open convex domain lies inside an exhaustion cube, and both the H¹ membership and the weak equation restrict to an open subset, so the same two statements hold on the domain with no new analysis. Subtracting the Green potential of the same residual on the domain leaves the harmonic part of the whole-space resolvent there: it is weakly a-harmonic on the domain and differs from psi by a named zero-trace Sobolev function.

This is the statement of ExitMeanValueIdentificationWhole.lean with the exhaustion cube replaced by an arbitrary bounded open convex domain; the Caccioppoli Cauchy estimate and the exhaustion limit are consumed through the cube statement and are not repeated.

The whole-space resolvent on a bounded part domain

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_h1Function_analyticMinimalResolventReal_part {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ∃ (z : HCPolySupport.H1Function V), z.toFun = A.analyticMinimalResolventReal mu f hf hfD ∧ IsScalarForcedWeakSolution A.a V (A.wholeSpaceResidual mu hf hfD) z

The whole-space resolvent is an H¹ function of every bounded part domain and solves the shifted equation there. Its value function is the exact continuous representative of the resolvent, not merely a function almost everywhere equal to it.

The harmonic part

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

The harmonic part of the whole-space resolvent on a bounded part domain: the resolvent less the Green potential of its residual.

Equations

• A.partWholeSpaceHarmonicPart hV mu hf hD hfD y = A.analyticMinimalResolventReal mu f hf hfD y - A.partGreenPotential hV (A.wholeSpaceResidual mu hf hfD) ⋯ ⋯ ⋯ y

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_h1Function_partWholeSpaceHarmonicPart {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ∃ (h : HCPolySupport.H1Function V), h.toFun = A.partWholeSpaceHarmonicPart hV mu hf hD hfD ∧ IsScalarForcedWeakSolution A.a V (fun (x : HCPolySupport.Vec d) => 0) h ∧ ∀ (y : HCPolySupport.Vec d), A.analyticMinimalResolventReal mu f hf hfD y - h.toFun y = (A.partGreenH10 hV ⋯ ⋯ ⋯).toFun y

The harmonic part of the whole-space resolvent is weakly a-harmonic on the part domain, and differs from the whole-space resolvent by a named zero-trace Sobolev function.