CruxUpperIdentities

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

The signed penalized identities

The resolvent identity and the subtraction-free perturbation identity of the whole-space exterior-penalized resolvent are proved on nonnegative data. The comparison family of the process layer acts on signed bounded measurable observables, so this module transports both identities to the signed real form by splitting the datum into its positive and negative parts.

The perturbation identity is stated in its subtracted form against the signed real analytic minimal resolvent, which is the shape the process layer consumes.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal_eq_of_eq {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (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.analyticMinimalResolventReal mu f hf hfD x = A.analyticMinimalResolventReal mu g hg hgE x

Equal data have the same signed real minimal resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal_sub {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {u v : HCPolySupport.Vec d → ℝ} (hu : Measurable u) (hv : Measurable v) {C E B : ℝ} (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.analyticMinimalResolventReal mu (fun (y : HCPolySupport.Vec d) => u y - v y) ⋯ huvB x = A.analyticMinimalResolventReal mu u hu huC x - A.analyticMinimalResolventReal mu v hv hvE x

The signed real minimal resolvent is subtractive.

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

The signed penalized resolvent identity. The exterior-penalized resolvents at two shifts differ by the composed resolvent, on signed bounded measurable data.

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

The signed subtraction-free perturbation identity. The signed real exterior-penalized resolvent is the minimal resolvent of the datum minus the minimal resolvent of the penalized load.