PartTorsion

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

The shift-uniform bound of the Dirichlet resolvent of a bounded part domain

The vanishing-shift limit of the Dirichlet resolvents of a fixed bounded datum exists because the resolvents are bounded uniformly in the shift and are Lipschitz in the shift. On an exhaustion cube both facts come from the torsion function of that cube. A general bounded part domain has no torsion function of its own here, and none is constructed: the domain is bounded, so it lies inside an exhaustion cube, and the Dirichlet resolvent of a nonnegative datum on the smaller domain is below the Dirichlet resolvent of the same datum on the larger one.

• partC0Resolvent_le_analyticCubeResolvent is that domain monotonicity. It is the weak maximum principle of PartDomainSubsolution.lean, which is already stated for an arbitrary bounded open convex domain inside another, read through the continuous representatives.
• partTorsionBound is the torsion bound of the containing exhaustion cube, and abs_partC0Resolvent_le_partTorsionBound bounds the Dirichlet resolvent of a datum bounded by D by D times it, uniformly in the shift.
• abs_partC0Resolvent_sub_le is the Lipschitz estimate in the shift, obtained from the uniform bound and the resolvent identity exactly as on an exhaustion cube.

Domain monotonicity

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_le_analyticCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {m : ℕ} (hVU : V ⊆ wholeSpaceCube d m) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ f z) {D : ℝ} (hfD : ∀ (z : HCPolySupport.Vec d), |f z| ≤ D) {x : HCPolySupport.Vec d} (hx : x ∈ V) : A.partC0Resolvent hV lam f hf hfD x ≤ A.analyticCubeResolvent lam f hf hfD m x

The Dirichlet resolvent of a nonnegative datum increases with the domain. On a bounded open convex domain inside an exhaustion cube, the zero extension of the part solution is a weak subsolution with the same forcing, so it lies below the solution on the cube; both sides are continuous on the part domain, so the inequality holds at every point of it.

The shift-uniform bound

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partTorsionBound {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) : ℝ

The torsion bound of an exhaustion cube containing a bounded part domain.

Equations

• A.partTorsionBound hV = A.cubeTorsionBound (DivergenceFormProcess.Form.partCubeIndex hV)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partTorsionBound_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) : 0 ≤ A.partTorsionBound hV

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_partC0Resolvent_le_partTorsionBound {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (z : HCPolySupport.Vec d), |f z| ≤ D) (x : HCPolySupport.Vec d) : |A.partC0Resolvent hV lam f hf hfD x| ≤ D * A.partTorsionBound hV

The Dirichlet resolvent of a bounded datum on a bounded part domain is bounded uniformly in the shift. Comparison with the constant datum of a containing exhaustion cube, whose Dirichlet resolvents are below the torsion function of that cube at every shift, replaces the shift-dependent bound D / lam by D times the torsion bound of the cube.

The Lipschitz estimate in the shift

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_partC0Resolvent_sub_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (lam nu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (z : HCPolySupport.Vec d), |f z| ≤ D) (x : HCPolySupport.Vec d) : |A.partC0Resolvent hV lam f hf hfD x - A.partC0Resolvent hV nu f hf hfD x| ≤ D * (A.partTorsionBound hV * A.partTorsionBound hV) * |↑lam - ↑nu|

The Dirichlet resolvents of a bounded datum on a bounded part domain are Lipschitz in the shift. The resolvent identity writes the difference of the values at two shifts as the difference of the shifts times a third Dirichlet resolvent, and the uniform bound applies twice to that third resolvent.