ResolventIdentity

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

Resolvent identity for the analytic cubic supremum

The bounded-domain resolvent identity is passed through the cubic exhaustion. The only analytic continuity input is the already proved convergence of interior representatives along uniformly bounded pointwise-convergent data.

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

The real local cube resolvents increase to the real value of their extended-real supremum on nonnegative bounded data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_analyticCubeResolvent_comp {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu nu : ↑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) (outer : ℕ) (x : HCPolySupport.Vec d) : let g := fun (y : HCPolySupport.Vec d) => (A.analyticMinimalResolvent mu f hf hfD y).toReal; Filter.Tendsto (fun (k : ℕ) => A.analyticCubeResolvent nu (A.analyticCubeResolvent mu f hf hfD k) ⋯ ⋯ outer x) Filter.atTop (nhds (A.analyticCubeResolvent nu g ⋯ ⋯ outer x))

Applying a fixed outer cube resolvent commutes with the monotone limit of the inner cubic exhaustion.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_resolventEquation {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (lam 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.analyticCubeResolvent lam f hf hfD m x = A.analyticCubeResolvent mu f hf hfD m x + (↑mu - ↑lam) * A.analyticCubeResolvent lam (A.analyticCubeResolvent mu f hf hfD m) ⋯ ⋯ m x

The bounded-domain identity in the orientation used by the abstract minimal-resolvent interface.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent_comp_eq_iSup {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (lam 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) : let g := fun (y : HCPolySupport.Vec d) => (A.analyticMinimalResolvent mu f hf hfD y).toReal; (A.analyticMinimalResolvent lam g ⋯ ⋯ x).toReal = ⨆ (n : ℕ), A.analyticCubeResolvent lam (A.analyticCubeResolvent mu f hf hfD n) ⋯ ⋯ n x

The diagonal of the two cubic exhaustions computes the composition of the two analytic minimal resolvents on nonnegative bounded data.

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

The real values of the nonnegative analytic minimal resolvent satisfy the resolvent equation.