PenalizedIdentities

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

Local identities for the whole-space penalized exhaustion

The algebraic resolvent and perturbation identities are first proved on one exhaustion cube. They use only the continuous-coefficient representative; small contrast is not part of these identities.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeLoad {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 potential load of a local exterior-penalized resolvent.

Equations

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

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedLoad {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) : ℝ

The potential load of the minimal whole-space exterior-penalized resolvent.

Equations

• A.analyticPenalizedLoad hV n mu f hf hfD x = DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential V n x * (A.analyticPenalizedResolvent hV n mu f hf hfD x).toReal

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticPenalizedCubeLoad {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.analyticPenalizedCubeLoad hV n mu f hf hfD m)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticPenalizedLoad {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.analyticPenalizedLoad hV n mu f hf hfD)

The whole-space penalized load is measurable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeLoad_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.analyticPenalizedCubeLoad hV n mu f hf hfD m x

A local penalized load is nonnegative for nonnegative data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticPenalizedCubeLoad_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.analyticPenalizedCubeLoad hV n mu f hf hfD m x| ≤ ↑n * (D / ↑mu)

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

The whole-space penalized load is nonnegative.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticPenalizedLoad_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.analyticPenalizedLoad hV n mu f hf hfD x| ≤ ↑n * (D / ↑mu)

The whole-space penalized load has the product of the potential bound and the resolvent maximum-principle bound as a uniform bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_perturbation {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 + A.analyticCubeResolvent mu (A.analyticPenalizedCubeLoad hV n mu f hf hfD m) ⋯ ⋯ m x = A.analyticCubeResolvent mu f hf hfD m x

The subtraction-free perturbation identity on one exhaustion cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolvent_perturbation {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).toReal + (A.analyticMinimalResolvent mu (A.analyticPenalizedLoad hV n mu f hf hfD) ⋯ ⋯ x).toReal = (A.analyticMinimalResolvent mu f hf hfD x).toReal

The subtraction-free perturbation identity passes to the whole-space exhaustion for nonnegative bounded data.

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

The resolvent identity for a fixed exterior penalty on one exhaustion cube.