RealResolvent

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

Signed real algebra for the analytic minimal resolvent

The signed real minimal resolvent is the limit of the signed zero-extended cube resolvents. Cube linearity yields additivity and homogeneity of the limit, together with the sharp maximum-principle bound.

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

Scalar multiplication commutes with one local analytic cube resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_eq_of_eqOn {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (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) (m : ℕ) (hfg : Set.EqOn f g (wholeSpaceCube d m)) (x : HCPolySupport.Vec d) : A.analyticCubeResolvent mu f hf hfD m x = A.analyticCubeResolvent mu g hg hgE m x

A local cube resolvent depends only on the datum restricted to that cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_analyticCubeResolvent_real {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (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.analyticCubeResolvent mu f hf hfD m x) Filter.atTop (nhds (A.analyticMinimalResolventReal mu f hf hfD x))

The signed zero-extended cube resolvents converge to the real minimal resolvent.

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

The real analytic minimal resolvent is additive.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal_smul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (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.analyticMinimalResolventReal mu (fun (y : HCPolySupport.Vec d) => c * f y) ⋯ ⋯ x = c * A.analyticMinimalResolventReal mu f hf hfD x

Scalar multiplication commutes with the real analytic minimal resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticMinimalResolventReal_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (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.analyticMinimalResolventReal mu f hf hfD x| ≤ D / ↑mu

The signed real analytic minimal resolvent has the sharp maximum-principle bound inherited from every cube.

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

The value of the real minimal resolvent is independent of the numerical bound used to certify boundedness of its datum.