ExcessiveMinimalMaximum

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

The maximum principle for the whole-space barrier

The truncated barriers increase to the whole-space barrier, and one fixed cube resolvent is continuous along a uniformly bounded pointwise convergent sequence of observables. Applying a fixed cube resolvent to the whole-space barrier is therefore the limit of applying it to the truncated barriers; each of those is dominated, by monotonicity in the cube index, by the cube resolvent at the index of the truncation, where the maximum principle of the previous step applies.

Taking the supremum over the exhaustion gives the maximum principle for the analytic minimal resolvent:

mu R^min_mu v <= mu / (mu - lam) * v for every mu > lam,

at every point of the whole space. This is exactly the resolvent hypothesis of the exponential comparison used to produce lam-excessive functions.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_analyticCubeResolvent_of_tendsto {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (nu : ↑MarkovProcess.Semigroup.PositiveShift) {gk : ℕ → HCPolySupport.Vec d → ℝ} {g : HCPolySupport.Vec d → ℝ} (hgk : ∀ (k : ℕ), Measurable (gk k)) (hg : Measurable g) {C : ℝ} (hC : 0 ≤ C) (hgkC : ∀ (k : ℕ) (y : HCPolySupport.Vec d), |gk k y| ≤ C) (hgC : ∀ (y : HCPolySupport.Vec d), |g y| ≤ C) (hconv : ∀ (y : HCPolySupport.Vec d), Filter.Tendsto (fun (k : ℕ) => gk k y) Filter.atTop (nhds (g y))) (m : ℕ) (x : HCPolySupport.Vec d) : Filter.Tendsto (fun (k : ℕ) => A.analyticCubeResolvent nu (gk k) ⋯ ⋯ m x) Filter.atTop (nhds (A.analyticCubeResolvent nu g hg ⋯ m x))

One cube resolvent is continuous along uniformly bounded pointwise convergent data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_congr_ae {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) (hfg : f =ᵐ[MeasureTheory.volume] g) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticCubeResolvent mu f hf hfD m x = A.analyticCubeResolvent mu g hg hgE m x

One cube resolvent depends only on the almost-everywhere class of its observable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent_congr_ae {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) (hfg : f =ᵐ[MeasureTheory.volume] g) (x : HCPolySupport.Vec d) : A.analyticMinimalResolvent mu f hf hfD x = A.analyticMinimalResolvent mu g hg hgE x

The minimal resolvent depends only on the almost-everywhere class of its observable.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.barrierBound_nonneg {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : 0 ≤ 2 * (P.D / ↑P.lam)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.mul_analyticCubeResolvent_barrier_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : ↑P.lam < ↑mu) (n : ℕ) (x : HCPolySupport.Vec d) : ↑mu * A.analyticCubeResolvent mu P.barrier ⋯ ⋯ n x ≤ ↑mu / (↑mu - ↑P.lam) * P.barrier x

The maximum principle for the whole-space barrier, on one cube.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.mul_analyticMinimalResolvent_barrier_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : ↑P.lam < ↑mu) (x : HCPolySupport.Vec d) : ↑mu * (A.analyticMinimalResolvent mu P.barrier ⋯ ⋯ x).toReal ≤ ↑mu / (↑mu - ↑P.lam) * P.barrier x

The maximum principle for the whole-space barrier.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.mul_analyticMinimalResolventReal_barrier_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : ↑P.lam < ↑mu) (x : HCPolySupport.Vec d) : ↑mu * A.analyticMinimalResolventReal mu P.barrier ⋯ ⋯ x ≤ ↑mu / (↑mu - ↑P.lam) * P.barrier x

The maximum principle in the signed form of the minimal resolvent.