ExitMeanValueCubeSetAt

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

The Dirichlet resolvent of a bounded part domain, read on a translated triadic cube

The exit decomposition of a resolvent datum needs the Dirichlet resolvent of the domain the process is killed on. On the centred exhaustion cubes that object is analyticCubeResolvent, whose index is the exhaustion step; the localized Dirichlet problems of the field are posed instead on cubeSetAt y n, the open cube of side 3 ^ n centred at y, which is not an exhaustion cube.

This file supplies the Dirichlet resolvent of an arbitrary bounded part domain and specializes it to a translated triadic cube.

• partC0Resolvent is the continuous representative of the Dirichlet resolvent of a bounded measurable datum on a bounded convex open set, extended by zero. It is the domain-generic form of analyticCubeResolvent: the underlying analytic object, continuousCoeffBoundedResolvent, already takes an arbitrary such set, and the ellipticity certificate is the one partEllipticity supplies for it.
• eq_partC0Resolvent_of_isRepresentative names it: a continuous function agreeing almost everywhere on the domain with the shifted part solution is that resolvent there.
• cubeSetAtC0Resolvent is that resolvent on cubeSetAt y n, with cubeSetAtC0BarrierData packaging the barrier data of the cube problem. The triadic cube is an axis cube, so the caller obligation of the whole-space barrier data is discharged there.

Everything here is analytic: no process, and no hypothesis about one, appears.

The datum of a translated triadic cube

noncomputable def DivergenceFormProcess.Form.cubeSetAtC0Datum {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : HCPolySupport.Vec d → ℝ

The restriction to a translated triadic cube of a continuous datum vanishing at infinity, extended by zero.

Equations

• DivergenceFormProcess.Form.cubeSetAtC0Datum y n g = (Algsuperdiff.Section5.Support.cubeSetAt y n).indicator fun (z : HCPolySupport.Vec d) => g z

theorem DivergenceFormProcess.Form.measurable_cubeSetAtC0Datum {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : Measurable (cubeSetAtC0Datum y n g)

theorem DivergenceFormProcess.Form.abs_cubeSetAtC0Datum_le {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (z : HCPolySupport.Vec d) : |cubeSetAtC0Datum y n g z| ≤ ‖g‖

theorem DivergenceFormProcess.Form.cubeSetAtC0Datum_nonneg {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) {g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ} (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) (z : HCPolySupport.Vec d) : 0 ≤ cubeSetAtC0Datum y n g z

theorem DivergenceFormProcess.Form.cubeSetAtC0Datum_of_mem {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) {z : HCPolySupport.Vec d} (hz : z ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : cubeSetAtC0Datum y n g z = g z

theorem DivergenceFormProcess.Form.cubeSetAtC0Datum_ae_indicator {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : cubeSetAtC0Datum y n g =ᵐ[MeasureTheory.volume] (Algsuperdiff.Section5.Support.cubeSetAt y n).indicator (cubeSetAtC0Datum y n g)

The Dirichlet resolvent of a bounded part domain

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.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) : HCPolySupport.Vec d → ℝ

The Dirichlet resolvent of a bounded part domain. The continuous representative supplied by freezing the skew part, extended by zero off the domain. This is analyticCubeResolvent with the exhaustion index replaced by the domain itself.

Equations

• A.partC0Resolvent hV mu f hf hfD = V.indicator (DivergenceFormProcess.Form.continuousCoeffBoundedResolvent A.a hV ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ mu ⋯ ⋯)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_of_mem {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) {x : HCPolySupport.Vec d} (hx : x ∈ V) : A.partC0Resolvent hV mu f hf hfD x = continuousCoeffBoundedResolvent A.a hV ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ mu ⋯ ⋯ x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_of_notMem {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) {x : HCPolySupport.Vec d} (hx : x ∉ V) : A.partC0Resolvent hV mu f hf hfD x = 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuousOn_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) : ContinuousOn (A.partC0Resolvent hV mu f hf hfD) V

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partC0Resolvent_ae {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) : A.partC0Resolvent hV mu f hf hfD =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (partDatumL2 hV hf hfD))

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

The Dirichlet resolvent of a part domain is nonnegative on a nonnegative datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.eq_partC0Resolvent_of_isRepresentative {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 : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {u : HCPolySupport.Vec d → ℝ} (hucont : Continuous u) (hurep : u =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ ⋯) (partDatumL2 hV hf hfD)))) {x : HCPolySupport.Vec d} (hx : x ∈ V) : u x = A.partC0Resolvent hV lam f hf hfD x

The Dirichlet resolvent of a part domain is named by continuity and its almost-everywhere value. A continuous function agreeing almost everywhere on the domain with the shifted part solution equals the resolvent at every point of the domain.

The Dirichlet resolvent of a translated triadic cube

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0BarrierData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) : WholeSpaceBarrierData A

The barrier data of the cube problem for a nonnegative continuous datum on a translated triadic cube.

Equations

• A.cubeSetAtC0BarrierData y n lam g hg0 = DivergenceFormProcess.Form.eqAxisCubeBarrierData A ⋯ (fun (i : Fin d) => y i - 3 ^ n / 2) ⋯ ⋯ lam ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0BarrierData_V {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) : (A.cubeSetAtC0BarrierData y n lam g hg0).V = Algsuperdiff.Section5.Support.cubeSetAt y n

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0BarrierData_f {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) : (A.cubeSetAtC0BarrierData y n lam g hg0).f = cubeSetAtC0Datum y n g

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0BarrierData_lam {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) : (A.cubeSetAtC0BarrierData y n lam g hg0).lam = lam

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0Resolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (lam : ℝ) : HCPolySupport.Vec d → ℝ

The Dirichlet resolvent of a continuous datum on a translated triadic cube, as a function of the shift; the value at a non-positive shift is zero.

Equations

• A.cubeSetAtC0Resolvent y n g lam = if h : 0 < lam then A.partC0Resolvent ⋯ ⟨lam, h⟩ (DivergenceFormProcess.Form.cubeSetAtC0Datum y n g) ⋯ ⋯ else 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0Resolvent_of_pos {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) {lam : ℝ} (hlam : 0 < lam) (x : HCPolySupport.Vec d) : A.cubeSetAtC0Resolvent y n g lam x = A.partC0Resolvent ⋯ ⟨lam, hlam⟩ (cubeSetAtC0Datum y n g) ⋯ ⋯ x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtC0Resolvent_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) {g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ} (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) (lam : ℝ) (x : HCPolySupport.Vec d) : 0 ≤ A.cubeSetAtC0Resolvent y n g lam x