PenalizedMinimal

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

Minimal whole-space resolvents with exterior penalization

For an open bounded convex cube V, the potential is n on Vᶜ and zero on V. The local potential resolvents increase along the cubic exhaustion, so their pointwise supremum defines the whole-space penalized resolvent.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential {d : ℕ} (V : Set (HCPolySupport.Vec d)) (n : ℕ) : HCPolySupport.Vec d → ℝ

The exterior penalization potential n 1_(Vᶜ).

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential V n = Vᶜ.indicator fun (x : HCPolySupport.Vec d) => ↑n

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_wholeSpacePenalizationPotential {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) : Measurable (wholeSpacePenalizationPotential V n)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential_nonneg {d : ℕ} (V : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : 0 ≤ wholeSpacePenalizationPotential V n x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential_le {d : ℕ} (V : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : wholeSpacePenalizationPotential V n x ≤ ↑n

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential_eq_zero {d : ℕ} {V : Set (HCPolySupport.Vec d)} (n : ℕ) {x : HCPolySupport.Vec d} (hx : x ∈ V) : wholeSpacePenalizationPotential V n x = 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential_isBounded {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n m : ℕ) : IsBoundedNonnegativePotential (wholeSpaceCube d m) (wholeSpacePenalizationPotential V n) ↑n

The exterior potential is bounded and nonnegative on every exhaustion cube.

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

The local potential resolvent on an exhaustion cube, extended by zero.

Equations

• One or more equations did not get rendered due to their size.

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

The extended-real local penalized resolvent.

Equations

• A.analyticPenalizedCubeResolventENN hV n mu f hf hfD m x = ENNReal.ofReal (A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x)

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

The minimal whole-space exterior-penalized resolvent.

Equations

• A.analyticPenalizedResolvent hV n mu f hf hfD x = ⨆ (m : ℕ), A.analyticPenalizedCubeResolventENN hV n mu f hf hfD m x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (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) (m : ℕ) (x : HCPolySupport.Vec d) : 0 ≤ A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x

Local penalized cube resolvents are nonnegative on nonnegative data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_mono {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (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) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x ≤ A.analyticPenalizedCubeResolvent hV n mu g hg hgE m x

A local penalized cube resolvent preserves pointwise order of bounded measurable data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_le_succ {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (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) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x ≤ A.analyticPenalizedCubeResolvent hV n mu f hf hfD (m + 1) x

The local exterior-penalized resolvents increase with the exhaustion.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.monotone_analyticPenalizedCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (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) : Monotone fun (m : ℕ) => A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x

At each point the local penalized resolvents form a monotone sequence.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_smul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (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) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticPenalizedCubeResolvent hV n mu (fun (y : HCPolySupport.Vec d) => c * f y) ⋯ hcf m x = c * A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x

Scalar multiplication commutes with one local exterior-penalized resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticPenalizedCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : Measurable (A.analyticPenalizedCubeResolvent hV n mu f hf hfD m)

A zero-extended local penalized resolvent is measurable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuousOn_analyticPenalizedCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : ContinuousOn (A.analyticPenalizedCubeResolvent hV n mu f hf hfD m) (wholeSpaceCube d m)

A local penalized representative is continuous on its defining cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : A.analyticPenalizedCubeResolvent hV n mu f hf hfD m =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] ↑↑((potentialResolvent A.a ⋯ ⋯ ⋯ (wholeSpacePenalizationPotential V n) ⋯) (boundedMeasurableToScalarL2 ⋯ ⋯ ⋯))

On its cube, the local representative agrees almost everywhere with the potential resolvent class.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticPenalizedResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : Measurable (A.analyticPenalizedResolvent hV n mu f hf hfD)

The minimal penalized resolvent is measurable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticPenalizedCubeResolvent_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : |A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x| ≤ D / ↑mu

Local penalized resolvents obey the maximum-principle bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolvent_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {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) : A.analyticPenalizedResolvent hV n mu f hf hfD x ≤ ENNReal.ofReal (D / ↑mu)

The minimal penalized resolvent inherits the sharp uniform bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_analyticPenalizedCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {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) : Filter.Tendsto (fun (m : ℕ) => A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x) Filter.atTop (nhds (A.analyticPenalizedResolvent hV n mu f hf hfD x).toReal)

The local penalized representatives converge to the real value of their extended-real supremum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.toReal_analyticPenalizedResolvent_smul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {c : ℝ} (hc : 0 ≤ c) {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) : (A.analyticPenalizedResolvent hV n mu (fun (y : HCPolySupport.Vec d) => c * f y) ⋯ ⋯ x).toReal = c * (A.analyticPenalizedResolvent hV n mu f hf hfD x).toReal

Nonnegative scalar multiplication commutes with the real value of the minimal exterior-penalized resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_add {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (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) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticPenalizedCubeResolvent hV n mu (fun (y : HCPolySupport.Vec d) => f y + g y) ⋯ hfg m x = A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x + A.analyticPenalizedCubeResolvent hV n mu g hg hgE m x

A local penalized resolvent is additive.