LocalSplitBounds

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

Local constants for the split stream field

This module converts the logarithmic ball estimates for the two scale ranges into the precise layer hypotheses used by the localized weighted estimate. The negative shells are controlled through matrix action, while the divergence of the continuously differentiable nonnegative shells costs the explicit contraction factor sqrt d * d.

noncomputable def Algsuperdiff.Section5.Field.streamSplitObservationRadius {d : ℕ} (x : HCPolySupport.Vec d) (rho : ℝ) : ℝ

An origin-centred observation radius containing euclideanBall x rho.

Equations

• Algsuperdiff.Section5.Field.streamSplitObservationRadius x rho = 1 + HCPolySupport.euclideanNorm x + rho

noncomputable def Algsuperdiff.Section5.Field.streamFieldSmallLocalConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) (rho : ℝ) : ℝ

The local size constant for the negative-shell part.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamFieldLargeDivLocalConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) (rho : ℝ) : ℝ

The local divergence constant for the nonnegative-shell part.

Equations

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

theorem Algsuperdiff.Section5.Field.one_le_streamSplitObservationRadius {d : ℕ} {x : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) : 1 ≤ streamSplitObservationRadius x rho

theorem Algsuperdiff.Section5.Field.euclideanNorm_lt_streamSplitObservationRadius_of_mem {d : ℕ} {x y : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) (hy : y ∈ HCPolySupport.euclideanBall x rho) : HCPolySupport.euclideanNorm y < streamSplitObservationRadius x rho

theorem Algsuperdiff.Section5.Field.streamFieldSmallLocalConst_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {x : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) : 0 ≤ streamFieldSmallLocalConst M omega x rho

theorem Algsuperdiff.Section5.Field.streamFieldLargeDivLocalConst_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {x : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) : 0 ≤ streamFieldLargeDivLocalConst M omega x rho

theorem Algsuperdiff.Section5.Field.vecNormSq_matVecMul_streamFieldSmall_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {x y : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) (hy : y ∈ HCPolySupport.euclideanBall x rho) (v : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (HCPolySupport.matVecMul (streamFieldSmall omega y) v) ≤ streamFieldSmallLocalConst M omega x rho ^ 2 * HCPolySupport.vecNormSq v

The negative-shell part has the matrix-action bound required on a local transition layer.

theorem Algsuperdiff.Section5.Field.vecNormSq_skewFieldDiv_streamFieldLarge_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {x y : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) (hy : y ∈ HCPolySupport.euclideanBall x rho) : HCPolySupport.vecNormSq (DivergenceFormProcess.Decay.skewFieldDiv (streamFieldLarge omega) y) ≤ streamFieldLargeDivLocalConst M omega x rho ^ 2

The divergence of the nonnegative-shell part has the local squared-size bound required by the integration-by-parts estimate.