CruxUpperFamily

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

The whole-space penalized comparison family

The comparison family of the exterior penalization at index n is the signed real exterior-penalized resolvent on the live space, assembled at the added point with the resolvent of the observable there. The added point is absorbing, so its value is the observable's value divided by the shift, and the exterior potential vanishes there.

This module proves the four properties the killed-resolvent comparison consumes: measurability, boundedness, the resolvent identity, and the subtraction-free perturbation identity against the kernel resolvent of the compactified semigroup. The identification of the kernel resolvent with the analytic minimal resolvent is the named explicit hypothesis of the analytic layer.

theorem DivergenceFormProcess.Form.onePointKernelResolventReal_infty_eq_div {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {lam : ℝ} (hlam : 0 < lam) {G : OnePoint (HCPolySupport.Vec d) → ℝ} (hG : Measurable G) : R.onePointKernelSemigroup.kernelResolventReal lam G OnePoint.infty = G OnePoint.infty / lam

The real kernel resolvent at the added absorbing point divides by the shift.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedComparisonFamily {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (lam : ℝ) (F : OnePoint (HCPolySupport.Vec d) → ℝ) : OnePoint (HCPolySupport.Vec d) → ℝ

The whole-space penalized comparison family. On the live space it is the signed real exterior-penalized resolvent; at the added point it is the kernel resolvent of the observable there.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedComparisonFamily_coe {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {lam : ℝ} (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) (x : HCPolySupport.Vec d) : A.penalizedComparisonFamily hV n R lam F ↑x = A.analyticPenalizedResolventReal hV n ⟨lam, hlam⟩ (fun (y : HCPolySupport.Vec d) => F ↑y) ⋯ ⋯ x

At a live point the comparison family is the signed real exterior-penalized resolvent of the restricted observable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedComparisonFamily_infty {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {lam : ℝ} (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) : A.penalizedComparisonFamily hV n R lam F OnePoint.infty = R.onePointKernelSemigroup.kernelResolventReal lam F OnePoint.infty

At the added point the comparison family is the kernel resolvent of the observable there.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_penalizedComparisonFamily {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {lam : ℝ} (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) : Measurable (A.penalizedComparisonFamily hV n R lam F)

The comparison family is measurable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_penalizedComparisonFamily_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {lam : ℝ} (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) (z : OnePoint (HCPolySupport.Vec d)) : |A.penalizedComparisonFamily hV n R lam F z| ≤ E / lam

The comparison family inherits the sharp maximum-principle bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedComparisonFamily_comp_coe {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {lam : ℝ} (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) : (fun (y : HCPolySupport.Vec d) => A.penalizedComparisonFamily hV n R lam F ↑y) = A.analyticPenalizedResolventReal hV n ⟨lam, hlam⟩ (fun (y : HCPolySupport.Vec d) => F ↑y) ⋯ ⋯

The live restriction of the comparison family is the signed real exterior-penalized resolvent of the live restriction of the observable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedComparisonFamily_resolventIdentity {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) {mu lam : ℝ} (hmu : 0 < mu) (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) : A.penalizedComparisonFamily hV n R mu F = A.penalizedComparisonFamily hV n R lam F + (lam - mu) • A.penalizedComparisonFamily hV n R lam (A.penalizedComparisonFamily hV n R mu F)

The resolvent identity of the comparison family.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedComparisonFamily_perturbation {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hcons : R.kernelSemigroup.IsConservative) (hid : A.KernelResolventIdentifiesAnalyticMinimal R) {lam : ℝ} (hlam : 0 < lam) {F : OnePoint (HCPolySupport.Vec d) → ℝ} (hF : Measurable F) {E : ℝ} (hFE : ∀ (z : OnePoint (HCPolySupport.Vec d)), |F z| ≤ E) : A.penalizedComparisonFamily hV n R lam F = R.onePointKernelSemigroup.kernelResolventReal lam F - R.onePointKernelSemigroup.kernelResolventReal lam fun (y : OnePoint (HCPolySupport.Vec d)) => onePointRealExtension (wholeSpacePenalizationPotential V n) y * A.penalizedComparisonFamily hV n R lam F y

The perturbation identity of the comparison family. The family solves the same bounded-potential perturbation equation as the real kernel resolvent of the compactified semigroup.