ShiftAsymptotics

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

Large-shift asymptotics of the stream tail profile

The cubic logarithmic cutting radius is negligible compared with the natural square-root resolvent scale. Consequently every fixed positive spatial radius eventually lies in the stretched-exponential branch of the uniform profile, where that profile tends to zero.

theorem Algsuperdiff.Section5.Field.tendsto_streamUniformExhaustionCutoff_div_sqrt {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : Filter.Tendsto (fun (mu : ↑MarkovProcess.Semigroup.PositiveShift) => streamUniformExhaustionCutoff M omega ↑mu / √↑mu) Filter.atTop (nhds 0)

The cubic logarithmic cutoff divided by the square-root mass tends to zero.

theorem Algsuperdiff.Section5.Field.tendsto_streamUniformExhaustionEnvelope_sqrt_mul {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {r : ℝ} (hr : 0 < r) : Filter.Tendsto (fun (mu : ↑MarkovProcess.Semigroup.PositiveShift) => streamUniformExhaustionEnvelope M omega (√↑mu * r)) Filter.atTop (nhds 0)

At every fixed positive spatial radius, the uniform envelope on the natural square-root scale tends to zero as the mass tends to infinity.

theorem Algsuperdiff.Section5.Field.eventually_streamUniformExhaustionCutoff_lt_sqrt_mul {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {r : ℝ} (hr : 0 < r) : ∀ᶠ (mu : ↑MarkovProcess.Semigroup.PositiveShift) in Filter.atTop, streamUniformExhaustionCutoff M omega ↑mu < √↑mu * r

A fixed positive radius eventually lies beyond the cubic logarithmic cutoff on the square-root mass scale.