PartResolventAlgebra

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

The algebra of the Dirichlet resolvent of a bounded part domain

partC0Resolvent is the Dirichlet resolvent of a bounded measurable datum on an arbitrary bounded open convex domain, extended by zero. This file records the elementary operations it supports, each one the domain-generic form of the corresponding statement about the resolvent of an exhaustion cube:

• partC0Resolvent_eq_of_eqOn — only the restriction of the datum to the domain is seen;
• abs_partC0Resolvent_le — the shift-dependent maximum-principle bound D / mu;
• partC0Resolvent_add, partC0Resolvent_smul, partC0Resolvent_add_const_mul — linearity in the datum;
• partC0Resolvent_mono — monotonicity in the datum;
• partC0Resolvent_resolvent_identity — the resolvent identity in the shift.

Every proof is the corresponding proof for an exhaustion cube with the cube replaced by the domain: the analytic representative continuousCoeffBoundedResolvent and all of its lemmas are already stated for an arbitrary bounded open convex domain, and the ellipticity certificate is the one partEllipticity supplies.

Measurability

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_partC0Resolvent {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 : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : Measurable (A.partC0Resolvent hV mu f hf hfD)

The Dirichlet resolvent of a part domain is measurable on the ambient space. It is the zero extension of the restriction to the domain of a function continuous there.

The datum is seen only on the domain

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_eq_of_eqOn {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hgE : ∀ (x : HCPolySupport.Vec d), |g x| ≤ E) (hfg : Set.EqOn f g V) (x : HCPolySupport.Vec d) : A.partC0Resolvent hV mu f hf hfD x = A.partC0Resolvent hV mu g hg hgE x

The Dirichlet resolvent of a part domain sees only the values of its datum on that domain.

The maximum-principle bound

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_partC0Resolvent_le {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) (x : HCPolySupport.Vec d) : |A.partC0Resolvent hV mu f hf hfD x| ≤ D / ↑mu

The shift-dependent maximum-principle bound of the Dirichlet resolvent of a part domain.

Linearity in the datum

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_add {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hgE : ∀ (x : HCPolySupport.Vec d), |g x| ≤ E) (hfg : ∀ (x : HCPolySupport.Vec d), |f x + g x| ≤ D + E) (x : HCPolySupport.Vec d) : A.partC0Resolvent hV mu (fun (y : HCPolySupport.Vec d) => f y + g y) ⋯ hfg x = A.partC0Resolvent hV mu f hf hfD x + A.partC0Resolvent hV mu g hg hgE x

The Dirichlet resolvent of a part domain is additive in its datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_smul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (c : ℝ) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hcf : ∀ (x : HCPolySupport.Vec d), |c * f x| ≤ |c| * D) (x : HCPolySupport.Vec d) : A.partC0Resolvent hV mu (fun (y : HCPolySupport.Vec d) => c * f y) ⋯ hcf x = c * A.partC0Resolvent hV mu f hf hfD x

The Dirichlet resolvent of a part domain is homogeneous in its datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_add_const_mul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (c : ℝ) {f h : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hh : Measurable h) {D E S : ℝ} (hfD : ∀ (y : HCPolySupport.Vec d), |f y| ≤ D) (hhE : ∀ (y : HCPolySupport.Vec d), |h y| ≤ E) (hs : Measurable fun (y : HCPolySupport.Vec d) => f y + c * h y) (hsS : ∀ (y : HCPolySupport.Vec d), |f y + c * h y| ≤ S) (x : HCPolySupport.Vec d) : A.partC0Resolvent hV mu (fun (y : HCPolySupport.Vec d) => f y + c * h y) hs hsS x = A.partC0Resolvent hV mu f hf hfD x + c * A.partC0Resolvent hV mu h hh hhE x

The Dirichlet resolvent of a part domain is affine in its datum.

Monotonicity in the datum

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_mono {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hgE : ∀ (x : HCPolySupport.Vec d), |g x| ≤ E) (hfg : ∀ (x : HCPolySupport.Vec d), f x ≤ g x) (x : HCPolySupport.Vec d) : A.partC0Resolvent hV mu f hf hfD x ≤ A.partC0Resolvent hV mu g hg hgE x

The Dirichlet resolvent of a part domain preserves pointwise order between bounded measurable data.

The resolvent identity in the shift

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

The resolvent identity for the Dirichlet resolvent of a part domain. The value at one shift is the value at another plus the difference of the shifts times the second resolvent of the first.