BoundaryGrowth

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

Logarithmic active-support constants on exhaustion cubes

The boundary cutoff on U_m requires coefficient control on its full topological support. That support lies in B(0,3^m). The stream field's rough-size and smooth-divergence constants there grow at most linearly in m, i.e. logarithmically in the physical radius.

noncomputable def Algsuperdiff.Section5.Field.streamBoundaryRoughConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : ℝ

Linear-in-scale envelope for the rough active-support constant.

Equations

• Algsuperdiff.Section5.Field.streamBoundaryRoughConst M omega = 2 * Algsuperdiff.Section5.Field.streamFieldSmallBallConst M omega

noncomputable def Algsuperdiff.Section5.Field.streamBoundarySmoothDivConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : ℝ

Linear-in-scale envelope for the smooth-divergence active-support constant.

Equations

• Algsuperdiff.Section5.Field.streamBoundarySmoothDivConst M omega = 2 * (√↑d * ↑d * Algsuperdiff.Section5.Field.streamFieldLargeGradientConst M omega)

theorem Algsuperdiff.Section5.Field.streamBoundaryRoughConst_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : 0 ≤ streamBoundaryRoughConst M omega

theorem Algsuperdiff.Section5.Field.streamBoundarySmoothDivConst_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : 0 ≤ streamBoundarySmoothDivConst M omega

theorem Algsuperdiff.Section5.Field.streamFieldSmallLocalConst_zero_triadic_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (m : ℕ) : streamFieldSmallLocalConst M omega 0 (3 ^ m) ≤ streamBoundaryRoughConst M omega * (↑m + 1)

The rough constant on the active cutoff support is at most linear in the exhaustion index.

theorem Algsuperdiff.Section5.Field.streamFieldLargeDivLocalConst_zero_triadic_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (m : ℕ) : streamFieldLargeDivLocalConst M omega 0 (3 ^ m) ≤ streamBoundarySmoothDivConst M omega * (↑m + 1)

The smooth-divergence constant on the active cutoff support is at most linear in the exhaustion index.