SubexponentialProfile

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

Log-subexponential tail profiles

This file supplies the deterministic integrability input for the localized stream-field resolvent tail. The profile has the form

C (1 + s₊)^n exp (-c s₊ / (1 + log (1 + s₊))),

where s₊ = max s 0. The natural algebraic prefactor is retained explicitly. The logarithmic denominator still leaves a finite cubic layer-cake integral.

noncomputable def Algsuperdiff.Section5.Field.logSubexponentialProfile (C c : ℝ) (n : ℕ) (s : ℝ) : ℝ

A log-subexponential profile with an explicit algebraic prefactor.

Equations

• Algsuperdiff.Section5.Field.logSubexponentialProfile C c n s = C * (1 + max s 0) ^ n * Real.exp (-c * max s 0 / (1 + Real.log (1 + max s 0)))

theorem Algsuperdiff.Section5.Field.logSubexponentialProfile_nonneg {C : ℝ} (hC : 0 ≤ C) (c : ℝ) (n : ℕ) (s : ℝ) : 0 ≤ logSubexponentialProfile C c n s

The profile is nonnegative when its amplitude is nonnegative.