WholeSpaceC0

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

Vanishing at infinity for the stream-field whole-space resolvent

The localized split-skew estimate is used at a radius proportional to the distance of the evaluation point from the origin. Radius amplification still leaves a fixed fraction of that distance between the evaluation ball and a compactly supported datum, while the uniform stretched-exponential envelope tends to zero. Sharp resolvent stability then extends the conclusion from compactly supported data to all continuous functions vanishing at infinity.

theorem Algsuperdiff.Section5.Field.tendsto_streamUniformExhaustionEnvelope_atTop {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : Filter.Tendsto (streamUniformExhaustionEnvelope M omega) Filter.atTop (nhds 0)

The common stretched-exponential envelope tends to zero at infinity.

theorem Algsuperdiff.Section5.Field.zero_at_infty_toReal_streamAnalyticMinimalResolvent {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : 1 ≤ ↑mu) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) (hfcompact : HasCompactSupport f) : Filter.Tendsto (fun (x : HCPolySupport.Vec d) => ((streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu f hf hf1 x).toReal) (Filter.cocompact (HCPolySupport.Vec d)) (nhds 0)

The positive analytic minimal resolvent of a normalized compactly supported datum vanishes at infinity for every shift at least one.

theorem Algsuperdiff.Section5.Field.zero_at_infty_toReal_streamAnalyticMinimalResolvent_of_compact {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : 1 ≤ ↑mu) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfcompact : HasCompactSupport f) : Filter.Tendsto (fun (x : HCPolySupport.Vec d) => ((streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu f hf hfD x).toReal) (Filter.cocompact (HCPolySupport.Vec d)) (nhds 0)

Scaling removes the normalization from a nonnegative compactly supported datum in the stream-field vanishing theorem.

theorem Algsuperdiff.Section5.Field.zero_at_infty_streamAnalyticMinimalResolventReal_of_compact {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : 1 ≤ ↑mu) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hfcompact : HasCompactSupport ⇑f) : Filter.Tendsto ((streamWholeSpaceAnalyticData M omega).analyticMinimalResolventReal mu ⇑f ⋯ ⋯) (Filter.cocompact (HCPolySupport.Vec d)) (nhds 0)

Compactly supported signed C₀ data have vanishing real resolvent for every shift at least one.

theorem Algsuperdiff.Section5.Field.hasVanishing_streamAnalyticMinimalResolvent {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : (streamWholeSpaceAnalyticData M omega).HasVanishingAnalyticMinimalResolvent

The stream-field analytic minimal resolvent maps every C₀ datum to a function vanishing at infinity.