ScaleDecompositionBounds

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

Logarithmic local bounds for the stream-field scale decomposition

The sharp carrier is read on the first triadic origin cube containing the Euclidean ball. Its crossover weight is linear in that cube scale, hence of order 1 + log R. Summation of the negative value rates and nonnegative gradient rates gives the two local constants of that decomposition.

noncomputable def Algsuperdiff.Section5.Field.streamObservationScale (R : ℝ) : ℕ

The first triadic scale whose side is at least 4 R.

Equations

• Algsuperdiff.Section5.Field.streamObservationScale R = ⌈Real.logb 3 (4 * R)⌉₊

noncomputable def Algsuperdiff.Section5.Field.streamLogWeight (R : ℝ) : ℝ

The logarithmic radial weight used by both halves of the field.

Equations

• Algsuperdiff.Section5.Field.streamLogWeight R = 1 + Real.log R

theorem Algsuperdiff.Section5.Field.streamLogWeight_pos {R : ℝ} (hR : 1 ≤ R) : 0 < streamLogWeight R

theorem Algsuperdiff.Section5.Field.mem_openOriginCube_streamObservationScale {d : ℕ} {R : ℝ} (hR : 1 ≤ R) {x : HCPolySupport.Vec d} (hx : √(HCPolySupport.vecNormSq x) ≤ R) : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑(streamObservationScale R))

noncomputable def Algsuperdiff.Section5.Field.streamSmallRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The geometric ratio for the small-scale stream contribution.

Equations

• Algsuperdiff.Section5.Field.streamSmallRatio M = Real.rpow 3 (-M.gamma)

noncomputable def Algsuperdiff.Section5.Field.streamLargeRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The geometric ratio for the large-scale stream contribution.

Equations

• Algsuperdiff.Section5.Field.streamLargeRatio M = Real.rpow 3 (M.gamma - 1)

noncomputable def Algsuperdiff.Section5.Field.streamSmallSeries {d : ℕ} (M : Section3.ABKModel d) : ℝ

The weighted geometric series for the small-scale stream contribution.

Equations

• Algsuperdiff.Section5.Field.streamSmallSeries M = ∑' (r : ℕ), (↑r + 1) * Algsuperdiff.Section5.Field.streamSmallRatio M ^ r

noncomputable def Algsuperdiff.Section5.Field.streamLargeSeries {d : ℕ} (M : Section3.ABKModel d) : ℝ

The weighted geometric series for the large-scale stream contribution.

Equations

• Algsuperdiff.Section5.Field.streamLargeSeries M = ∑' (r : ℕ), (↑r + 1) * Algsuperdiff.Section5.Field.streamLargeRatio M ^ r

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

A concrete sample constant for the logarithmic bound on the rough part.

Equations

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

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

A concrete sample constant for the logarithmic gradient bound on the smooth part.

Equations

• Algsuperdiff.Section5.Field.streamFieldLargeGradientConst M omega = 6 * ↑d * ↑(Algsuperdiff.Section5.Field.streamSharpConst M omega) * Algsuperdiff.Section5.Field.streamLargeSeries M

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

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

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamFieldSmall_le {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 (streamFieldSmall omega x) ≤ streamFieldSmallBallConst M omega * streamLogWeight R

On a Euclidean ball, the rough negative-shell part is bounded by a constant times 1 + log R.

theorem Algsuperdiff.Section5.Field.norm_streamFieldLargeDeriv_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {R : ℝ} (hR : 1 ≤ R) {x : HCPolySupport.Vec d} (hx : √(HCPolySupport.vecNormSq x) ≤ R) : ‖streamFieldLargeDeriv omega x‖ ≤ streamFieldLargeGradientConst M omega * streamLogWeight R

On a Euclidean ball, the gradient of the nonnegative-shell part is bounded by a constant times 1 + log R.