BoundaryConservativity

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

Conservativity of the stream-field analytic minimal resolvent

The split-skew constants on the active support of the cubic boundary cutoff grow at most linearly in the exhaustion index. The inward distance grows like 3^m, so the localized boundary defect still tends to zero. This file uses only the split datum of the model; no global small-contrast assumption is made.

noncomputable def Algsuperdiff.Section5.Field.streamBoundaryLocalizedUpperConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) : ℝ

A scale-independent upper coefficient for the localized Agmon constant on the active support of the cubic boundary cutoff.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Field.streamBoundaryLocalizedUpperConst_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) : 0 < streamBoundaryLocalizedUpperConst M omega mu

theorem Algsuperdiff.Section5.Field.localizedInteriorUpper_streamBoundary_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : DivergenceFormProcess.Decay.localizedInteriorUpper M.nu (↑mu) (streamFieldSmallLocalConst M omega 0 (3 ^ m)) (streamFieldLargeDivLocalConst M omega 0 (3 ^ m)) ≤ streamBoundaryLocalizedUpperConst M omega mu * (↑m + 1)

The effective localized upper constant grows at most linearly in the exhaustion index.

theorem Algsuperdiff.Section5.Field.tendsto_abs_streamAnalyticCubeBoundaryRemainder {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : Filter.Tendsto (fun (m : ℕ) => |1 - ↑mu * (streamWholeSpaceAnalyticData M omega).analyticCubeResolvent mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ m x|) Filter.atTop (nhds 0)

theorem Algsuperdiff.Section5.Field.ofReal_mul_streamAnalyticMinimalResolvent_one_eq {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : ENNReal.ofReal ↑mu * (streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ x = 1

The analytic minimal resolvent of the stream coefficient has the exact constant-one normalization.