CruxStreamInterchange

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

Localized-tail penalization interchange for the stream field

The generic lemma isolates the compact-domain penalization limit from the coefficient-dependent tail estimate. The stream specialization supplies the fixed-collar log-subexponential profile proved from localized split-skew data. No whole-space small-contrast datum occurs in this module.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.iInf_toReal_analyticPenalizedResolvent_le_cube_of_eventually_error {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d v) (error : ℕ → ℝ) (herror : Filter.Tendsto error Filter.atTop (nhds 0)) (hcompare : ∀ᶠ (n : ℕ) in Filter.atTop, (A.analyticPenalizedResolvent ⋯ n mu f hf hf1 x).toReal ≤ A.analyticPenalizedCubeResolvent ⋯ n mu f hf hf1 (v + 1) x + error n) : ⨅ (n : ℕ), (A.analyticPenalizedResolvent ⋯ n mu f hf hf1 x).toReal ≤ A.analyticCubeResolvent mu f hf hf1 v x

A coefficient-generic interchange lemma: any eventually valid next-cube comparison whose scalar error tends to zero yields the desired infimum bound.

theorem Algsuperdiff.Section5.Field.iInf_toReal_streamAnalyticPenalizedResolvent_le_cube {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) (hfsupp : ∀ᵐ (x : HCPolySupport.Vec d), x ∉ DivergenceFormProcess.Form.wholeSpaceCube d v → f x = 0) {x : HCPolySupport.Vec d} (hx : x ∈ DivergenceFormProcess.Form.wholeSpaceCube d v) : ⨅ (n : ℕ), ((streamWholeSpaceAnalyticData M omega).analyticPenalizedResolvent ⋯ n mu f hf hf1 x).toReal ≤ (streamWholeSpaceAnalyticData M omega).analyticCubeResolvent mu f hf hf1 v x

The normalized stream-field penalization interchange. Fixed-collar localized tails replace the unavailable global small-contrast estimate.

theorem Algsuperdiff.Section5.Field.iInf_toReal_streamAnalyticPenalizedResolvent_le_cube_of_bound {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) (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) (hfsupp : ∀ᵐ (x : HCPolySupport.Vec d), x ∉ DivergenceFormProcess.Form.wholeSpaceCube d v → f x = 0) {x : HCPolySupport.Vec d} (hx : x ∈ DivergenceFormProcess.Form.wholeSpaceCube d v) : ⨅ (n : ℕ), ((streamWholeSpaceAnalyticData M omega).analyticPenalizedResolvent ⋯ n mu f hf hfD x).toReal ≤ (streamWholeSpaceAnalyticData M omega).analyticCubeResolvent mu f hf hfD v x

The bounded stream-field penalization interchange, obtained by positive normalization.