Growth

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

Linear growth of the stream matrix

On a cube of scale ℓ the normalized field splits as k = (k_ℓ - k_ℓ(0)) + Σ_{n > ℓ} (j_n - j_n(0)). The first summand is bounded by twice the descending value sum on □_ℓ, the second by the diameter 3^{ℓ} of the cube times the ascending gradient sum on □_ℓ. The quantitative condition of the carrier bounds the first by C 3^{ℓ} and the second by C, so the size of the field on □_ℓ is at most a dimensional multiple of C 3^{ℓ}.

Choosing the smallest cube containing the ball of radius R turns this into the linear bound ‖k‖_{L^∞(B_R)} ≤ C_k (1 + R) for R ≥ 1, with the sample constant C_k displayed explicitly. The true growth of the source field is R^{γ}; the linear statement is the one the process theory consumes.

Main definitions

• streamTailConst ω — the sample constant supplied by the carrier.
• streamFieldGrowthConst ω — the explicit linear-growth constant.

Main results

• matrixOperatorNorm_streamField_le_on_cube — the cube form.
• matrixOperatorNorm_streamField_le — the linear growth on balls.

References

• ABK26, the stream matrix; the almost sure bound ‖k‖_{L^∞(U_m)} ≲ 3^{γ m}.

1. The matrix norm through the entries

2. The sample constant

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

The sample constant of the quantitative two-leg condition.

Equations

• Algsuperdiff.Section5.Field.streamTailConst M omega = Classical.choose ⋯

theorem Algsuperdiff.Section5.Field.streamTailConst_spec {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : StreamGrowthBounded (streamTailConst M omega) ↑omega

3. The two legs on one cube

4. The bound on a cube

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamField_le_on_cube {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (ell : ℕ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑ell)) : HCPolySupport.Book.Ch02.matrixOperatorNorm (streamField omega x) ≤ ↑d ^ 2 * (↑(streamTailConst M omega) * (2 + ↑d / 2)) * 3 ^ ell

The size of the field on the origin cube of scale ℓ.

5. Linear growth on balls

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

The explicit linear-growth constant of the normalized field: a dimensional factor times the sample constant of the carrier.

Equations

• Algsuperdiff.Section5.Field.streamFieldGrowthConst M omega = 6 * (↑d ^ 2 * (↑(Algsuperdiff.Section5.Field.streamTailConst M omega) * (2 + ↑d / 2)))

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

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamField_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {R : ℝ} (hR : 1 ≤ R) {x : HCPolySupport.Vec d} (hx : ‖x‖ ≤ R) : HCPolySupport.Book.Ch02.matrixOperatorNorm (streamField omega x) ≤ streamFieldGrowthConst M omega * (1 + R)

Linear growth: ‖k‖_{L^∞(B_R)} ≤ C_k (1 + R) for every R ≥ 1, with the sample constant C_k of streamFieldGrowthConst.

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamField_le_of_euclidean {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {R : ℝ} (hR : 1 ≤ R) {x : HCPolySupport.Vec d} (hx : √(HCPolySupport.vecNormSq x) ≤ R) : HCPolySupport.Book.Ch02.matrixOperatorNorm (streamField omega x) ≤ streamFieldGrowthConst M omega * (1 + R)

Linear growth on Euclidean balls, the form of the source's ‖k‖_{L^∞(B_R)} ≤ C_k (1 + R): the ambient supremum norm of Vec d is dominated by the Euclidean norm, so the ball statement follows from the cube statement with the same constant.