PartGreenPotential

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

The vanishing-shift limit of the Dirichlet resolvents of a bounded part domain

The Dirichlet resolvents R^V_lam f of a fixed bounded measurable datum on a bounded open convex domain converge as the shift decreases to zero. The two inputs are the shift-uniform bound and the Lipschitz estimate in the shift of PartTorsion.lean; a Lipschitz real family on the positive half-line converges as its argument decreases to zero, with an error proportional to the argument.

The limit is partGreenPotential; it vanishes off the domain, obeys the same uniform bound, is measurable, and is continuous on the domain, being a uniform limit there of the Dirichlet resolvents.

This is the statement of ExitMeanValueHarmonicPotential.lean with the exhaustion cube replaced by an arbitrary bounded open convex domain. The identification of partGreenPotential with the zero-trace weak solution of the unshifted Dirichlet problem is a separate question and is not addressed here.

The shift-indexed Dirichlet resolvent

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (f : HCPolySupport.Vec d → ℝ) (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (lam : ℝ) (x : HCPolySupport.Vec d) : ℝ

The Dirichlet resolvent of a bounded measurable datum on a bounded part domain, as a function of the shift; the value at a non-positive shift is zero.

Equations

• A.partShiftResolvent hV f hf hfD lam x = if h : 0 < lam then A.partC0Resolvent hV ⟨lam, h⟩ f hf hfD x else 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftResolvent_of_pos {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {lam : ℝ} (hlam : 0 < lam) (x : HCPolySupport.Vec d) : A.partShiftResolvent hV f hf hfD lam x = A.partC0Resolvent hV ⟨lam, hlam⟩ f hf hfD x

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftResolvent_of_notMem {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (lam : ℝ) {x : HCPolySupport.Vec d} (hx : x ∉ V) : A.partShiftResolvent hV f hf hfD lam x = 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftResolvent_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (lam : ℝ) (x : HCPolySupport.Vec d) : 0 ≤ A.partShiftResolvent hV f hf hfD lam x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftResolvent_eq_of_eqOn {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {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) (lam : ℝ) (x : HCPolySupport.Vec d) : A.partShiftResolvent hV f hf hfD lam x = A.partShiftResolvent hV g hg hgE lam x

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

The Lipschitz constant in the shift of the Dirichlet resolvents of a datum bounded by D on a bounded part domain.

Equations

• A.partGreenRate hV D = D * (A.partTorsionBound hV * A.partTorsionBound hV)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenRate_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {D : ℝ} (hD : 0 ≤ D) : 0 ≤ A.partGreenRate hV D

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_forall_abs_partShiftResolvent_sub_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : ∃ (c : ℝ), ∀ (lam : ℝ), 0 < lam → |A.partShiftResolvent hV f hf hfD lam x - c| ≤ A.partGreenRate hV D * lam

The Dirichlet resolvents of a fixed bounded datum on a bounded part domain converge as the shift decreases to zero. The limit is approached at a rate proportional to the shift.

The Green potential

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

The Green potential of a bounded measurable datum on a bounded part domain: the limit of its Dirichlet resolvents as the shift decreases to zero.

Equations

• A.partGreenPotential hV f hf hD hfD x = Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_partShiftResolvent_sub_partGreenPotential_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) {lam : ℝ} (hlam : 0 < lam) : |A.partShiftResolvent hV f hf hfD lam x - A.partGreenPotential hV f hf hD hfD x| ≤ A.partGreenRate hV D * lam

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_partShiftResolvent_nhdsGT_zero {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : Filter.Tendsto (fun (lam : ℝ) => A.partShiftResolvent hV f hf hfD lam x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A.partGreenPotential hV f hf hD hfD x))

The Dirichlet resolvents converge to the Green potential as the shift decreases to zero.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenPotential_of_notMem {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {x : HCPolySupport.Vec d} (hx : x ∉ V) : A.partGreenPotential hV f hf hD hfD x = 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_partGreenPotential_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : |A.partGreenPotential hV f hf hD hfD x| ≤ D * A.partTorsionBound hV

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenPotential_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : 0 ≤ A.partGreenPotential hV f hf hD hfD x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenPotential_eq_of_eqOn {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hD : 0 ≤ D) (hE : 0 ≤ 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.partGreenPotential hV f hf hD hfD x = A.partGreenPotential hV g hg hE hgE x

The Green potential of a part domain sees only the values of its datum on that domain.

Regularity of the Green potential

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendstoUniformlyOn_partShiftResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : TendstoUniformlyOn (fun (n : ℕ) => A.partShiftResolvent hV f hf hfD (↑n + 1)⁻¹) (A.partGreenPotential hV f hf hD hfD) Filter.atTop V

The Dirichlet resolvents converge to the Green potential uniformly on the domain. The rate of abs_partShiftResolvent_sub_partGreenPotential_le does not depend on the point.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuousOn_partGreenPotential {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ContinuousOn (A.partGreenPotential hV f hf hD hfD) V

The Green potential is continuous on the domain, being a uniform limit of the Dirichlet resolvents, which are continuous there.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_partGreenPotential {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : Measurable (A.partGreenPotential hV f hf hD hfD)