CruxStreamBarrier

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

Coefficient-generic C₀ data for the whole-space barrier

The lower crux comparison does not use global small contrast. Its coefficient-dependent inputs are precisely vanishing of the analytic minimal resolvent on C₀, dense range of that resolver, and vanishing for bounded nonnegative compactly supported data. The remaining inputs are supplied by WholeSpaceBarrierData: the axis-cube constructor and its continuous zero-extension witness are coefficient-generic consequences of the continuous skew field carried by WholeSpaceAnalyticData.

This module packages those inputs without changing the established small-contrast API. It supplies both the old small-contrast datum and the stream field as instances of the new definition-shaped structure.

structure DivergenceFormProcess.Form.WholeSpaceC0BarrierData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) : Prop

The exact coefficient-dependent C₀ and compact-data inputs used by the excessive-barrier half of the crux. Axis-cube barrier data and their continuity witnesses are already constructed from WholeSpaceAnalyticData and therefore are not additional fields.

• vanishing : A.HasVanishingAnalyticMinimalResolvent

  The analytic minimal resolvent maps C₀ to C₀.

• denseRange : A.HasDenseRangeAnalyticMinimalC0OfVanishing ⋯

  Every analytic minimal C₀ resolvent operator has dense range.

• compactVanishing (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (_hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : HasCompactSupport f → Filter.Tendsto (fun (x : HCPolySupport.Vec d) => (A.analyticMinimalResolvent mu f hf hfD x).toReal) (Filter.cocompact (HCPolySupport.Vec d)) (nhds 0)

  Positive bounded compactly supported data have resolvents vanishing at infinity at every positive shift.

noncomputable def DivergenceFormProcess.Form.WholeSpaceC0BarrierData.resolvent {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (B : WholeSpaceC0BarrierData A) : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)

The positive contractive resolver canonically assembled from the barrier data.

Equations

• B.resolvent = A.analyticMinimalPositiveC0ContractiveResolventOfVanishing ⋯ ⋯

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceC0BarrierData.resolvent_operator {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (B : WholeSpaceC0BarrierData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : (B.resolvent.operator mu) f = A.analyticMinimalC0ResolventOfVanishing ⋯ mu f

noncomputable def DivergenceFormProcess.Form.WholeSpaceBarrierData.barrierC0OfData {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ

The whole-space barrier as a C₀ function under the coefficient-generic barrier input.

Equations

• P.barrierC0OfData B = { toFun := P.barrier, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.barrierC0OfData_apply {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) (x : HCPolySupport.Vec d) : (P.barrierC0OfData B) x = P.barrier x

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.barrierC0OfData_nonneg {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) (x : HCPolySupport.Vec d) : 0 ≤ (P.barrierC0OfData B) x

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.analyticMinimalResolventReal_barrierC0OfData {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : (A.analyticMinimalC0ResolventOfVanishing ⋯ mu (P.barrierC0OfData B)) x = A.analyticMinimalResolventReal mu P.barrier ⋯ ⋯ x

Evaluation of the generic analytic C₀ resolver on the barrier.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.mul_operator_barrierC0OfData_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = A.analyticMinimalC0ResolventOfVanishing ⋯ mu g) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : ↑P.lam < ↑mu) (x : HCPolySupport.Vec d) : ↑mu * ((R.operator mu) (P.barrierC0OfData B)) x ≤ ↑mu / (↑mu - ↑P.lam) * (P.barrierC0OfData B) x

The resolvent inequality used by exponential comparison, with no global small-contrast input.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.isLambdaExcessive_onePointAssemble_barrierC0OfData {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = A.analyticMinimalC0ResolventOfVanishing ⋯ mu g) : R.onePointKernelSemigroup.IsLambdaExcessive (↑P.lam) (MarkovProcess.PositiveC0ContractiveResolvent.onePointAssemble (P.barrierC0OfData B) 0)

The assembled generic barrier is excessive for the one-point extension. This is the stopping input used by the S-free lower crux comparison.

theorem Algsuperdiff.Section5.Field.streamWholeSpaceC0BarrierData {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : DivergenceFormProcess.Form.WholeSpaceC0BarrierData (streamWholeSpaceAnalyticData M omega)

The stream field supplies the coefficient-generic barrier data entirely from the localized split-skew vanishing and dense-range theorems.