CruxUpperPenalizedReal

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

Signed real algebra for the whole-space exterior-penalized resolvent

The exterior-penalized resolvent of the cubic exhaustion is defined on nonnegative data as a supremum of extended reals. The comparison family required by the process layer acts on signed bounded measurable observables, so this module builds the signed real form as the difference of the values on the positive and negative parts, and transports cube linearity to it.

The pattern is the one already used for the analytic minimal resolvent: the signed zero-extended cube resolvents converge to the signed real value, and additivity, homogeneity, the sharp maximum-principle bound and independence of the numerical bound follow from the corresponding cube statements.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticPositivePart_le_of_bound {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : |analyticPositivePart f x| ≤ D

A bound for an observable bounds its nonnegative part.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPositivePart_sub_neg {d : ℕ} (f : HCPolySupport.Vec d → ℝ) : (fun (x : HCPolySupport.Vec d) => analyticPositivePart f x - analyticPositivePart (fun (y : HCPolySupport.Vec d) => -f y) x) = f

The nonnegative parts of an observable and of its negative reconstruct it.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_bound_irrel {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 E : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfE : ∀ (x : HCPolySupport.Vec d), |f x| ≤ E) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x = A.analyticPenalizedCubeResolvent hV n mu f hf hfE m x

The value of a local penalized representative does not depend on the numerical bound certifying boundedness of its datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_congr {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hfg : f = g) (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hgE : ∀ (x : HCPolySupport.Vec d), |g x| ≤ E) (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

Two equal data with possibly different bounds have the same local penalized representative.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCubeResolvent_eq_parts {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) : A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x = A.analyticPenalizedCubeResolvent hV n mu (analyticPositivePart f) ⋯ ⋯ m x - A.analyticPenalizedCubeResolvent hV n mu (analyticPositivePart fun (y : HCPolySupport.Vec d) => -f y) ⋯ ⋯ m x

A local penalized representative splits along the positive and negative parts of its datum.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolventReal {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 signed real whole-space exterior-penalized resolvent. It is the difference of the values on the positive and negative parts of the datum.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_analyticPenalizedCubeResolvent_real {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) : Filter.Tendsto (fun (m : ℕ) => A.analyticPenalizedCubeResolvent hV n mu f hf hfD m x) Filter.atTop (nhds (A.analyticPenalizedResolventReal hV n mu f hf hfD x))

The signed zero-extended penalized cube resolvents converge to the signed real whole-space penalized resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolventReal_eq_toReal {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) : A.analyticPenalizedResolventReal hV n mu f hf hfD x = (A.analyticPenalizedResolvent hV n mu f hf hfD x).toReal

On nonnegative data the signed real form is the real value of the extended-real penalized resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolventReal_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) (x : HCPolySupport.Vec d) : A.analyticPenalizedResolventReal hV n mu (fun (y : HCPolySupport.Vec d) => f y + g y) ⋯ ⋯ x = A.analyticPenalizedResolventReal hV n mu f hf hfD x + A.analyticPenalizedResolventReal hV n mu g hg hgE x

The signed real penalized resolvent is additive.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolventReal_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) (x : HCPolySupport.Vec d) : A.analyticPenalizedResolventReal hV n mu (fun (y : HCPolySupport.Vec d) => c * f y) ⋯ ⋯ x = c * A.analyticPenalizedResolventReal hV n mu f hf hfD x

Scalar multiplication commutes with the signed real penalized resolvent.

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

The signed real penalized resolvent inherits the sharp maximum-principle bound of every cube.

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

The signed real penalized resolvent does not depend on the numerical bound certifying boundedness of its datum.

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

Two data agreeing everywhere have the same signed real penalized resolvent.

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

The signed real penalized resolvent is measurable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolventReal_sub_of_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {u v : HCPolySupport.Vec d → ℝ} (hu : Measurable u) (hv : Measurable v) (hu0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ u x) (hv0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ v x) {B C E : ℝ} (huC : ∀ (x : HCPolySupport.Vec d), |u x| ≤ C) (hvE : ∀ (x : HCPolySupport.Vec d), |v x| ≤ E) (huvB : ∀ (x : HCPolySupport.Vec d), |u x - v x| ≤ B) (x : HCPolySupport.Vec d) : A.analyticPenalizedResolventReal hV n mu (fun (y : HCPolySupport.Vec d) => u y - v y) ⋯ huvB x = (A.analyticPenalizedResolvent hV n mu u hu huC x).toReal - (A.analyticPenalizedResolvent hV n mu v hv hvE x).toReal

The difference of the values on two nonnegative data is the value on their difference.