UniformExhaustionProfile

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

A shift-uniform exhaustion-tail profile

Radius amplification controls the polynomially growing pointwise amplitude in the far branch. In the complementary branch the starting point is bounded in terms of the shift and the dimensionless radius. The latter branch is placed beyond a cubic logarithmic cutoff. Both branches are then dominated by one cube-root stretched exponential with a shift-independent cubic budget.

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

The positive stretched-exponential rate used by the uniform profile.

Equations

• Algsuperdiff.Section5.Field.streamUniformExhaustionRate M omega = Algsuperdiff.Section5.Field.streamTailDecayConst M omega / 1000

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

The scale constant of the cubic-log cutoff.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamUniformShiftWeight (lam : ℝ) : ℝ

A positive logarithmic weight for every real shift parameter.

Equations

• Algsuperdiff.Section5.Field.streamUniformShiftWeight lam = 1 + Real.log (max lam 1)

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

The cubic-log cutting radius.

Equations

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

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

The common stretched-exponential majorant above the cutting radius.

Equations

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

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

The shift-dependent profile is trivial below its cutoff and equals the uniform envelope above it.

Equations

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

theorem Algsuperdiff.Section5.Field.streamUniformExhaustionCutoff_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (lam : ℝ) : 0 ≤ streamUniformExhaustionCutoff M omega lam

The cubic-log cutoff is nonnegative.

theorem Algsuperdiff.Section5.Field.one_le_streamUniformExhaustionCutoff {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (lam : ℝ) : 1 ≤ streamUniformExhaustionCutoff M omega lam

The cubic-log cutoff is at least one.

theorem Algsuperdiff.Section5.Field.streamUniformExhaustionProfile_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (lam s : ℝ) : 0 ≤ streamUniformExhaustionProfile M omega lam s

theorem Algsuperdiff.Section5.Field.one_le_streamUniformExhaustionProfile_of_le_cutoff {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {lam s : ℝ} (hs : s ≤ streamUniformExhaustionCutoff M omega lam) : 1 ≤ streamUniformExhaustionProfile M omega lam s

Below the cutting radius the uniform profile is the trivial unit bound.

theorem Algsuperdiff.Section5.Field.streamLocalizedTailProfile_amp_le_uniform {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {lam : ℝ} (hlam : 1 ≤ lam) (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (hs : streamUniformExhaustionCutoff M omega lam < √lam * r) : streamLocalizedTailProfile M omega x (√lam * streamExhaustionAmp x r) ≤ streamUniformExhaustionProfile M omega lam (√lam * r)

The per-point localized profile at the amplified radius is dominated by the shift-uniform profile above the cubic-log cutoff.