ProcessInterface

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

Interface from a cubic supremum resolvent to a whole-space process

This file records the exact abstract interface used after the analytic cubic supremum has been identified with a family of transported local resolvents. Continuity at infinity, dense range, conservativity, and the analytic penalized-resolvent properties remain explicit inputs.

structure DivergenceFormProcess.Form.PenalizedResolventFamilyAssumptions {alpha : Type u_1} [MeasurableSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (q : alpha → ℝ) (C : ℝ) (Y : ℝ → (alpha → ℝ) → alpha → ℝ) : Prop

The analytic obligations on a real penalized resolvent family used by the killed-resolvent comparison theorem.

• measurable {lam : ℝ} : 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (Y lam f)
• bounded {lam : ℝ} : 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → ∃ (D : ℝ), ∀ (x : alpha), |Y lam f x| ≤ D
• resolvent {mu lam : ℝ} : 0 < mu → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Y mu f = Y lam f + (lam - mu) • Y lam (Y mu f)
• perturbation {lam : ℝ} : C < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Y lam f = P.kernelResolventReal lam f - P.kernelResolventReal lam fun (y : alpha) => q y * Y lam f y

theorem DivergenceFormProcess.Form.killedResolvent_le_of_penalizedResolventFamily {alpha : Type u_1} [MetricSpace alpha] [LocallyCompactSpace alpha] [SecondCountableTopology alpha] [MeasurableSpace alpha] [BorelSpace alpha] [CompleteSpace alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {q : alpha → ℝ} (hq : Measurable q) (hqU : ∀ y ∈ U, q y = 0) {C : ℝ} (hq0 : ∀ (y : alpha), 0 ≤ q y) (hqC : ∀ (y : alpha), q y ≤ C) (Y : ℝ → (alpha → ℝ) → alpha → ℝ) (hY : PenalizedResolventFamilyAssumptions P q C Y) {f : alpha → ℝ} (hf : Measurable f) (hf0 : ∀ (y : alpha), 0 ≤ f y) {D : ℝ} (hfD : ∀ (y : alpha), |f y| ≤ D) {lam : ℝ} (hlam : 0 < lam) (x : alpha) : MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent P hP U hU lam (fun (y : alpha) => ENNReal.ofReal (f y)) x ≤ ENNReal.ofReal (Y lam f x)

A family satisfying the explicit analytic interface dominates the killed resolvent on every open set where its potential vanishes.