PthMomentProcessScale

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

Confinement-scale comparisons for the displacement minimum

The widened random scale controls every larger triadic scale. Combined with the intrinsic-scale identity, this bounds the random displacement scale by the two-branch deterministic minimum used in the stream-process tail estimate.

theorem Algsuperdiff.Section5.Provider.sq_div_intrinsicScale_le_displacementMinScale {nu cstar gamma t r : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma < 1) (hgc : gamma ≤ cstar) (ht : 0 < t) (hr : Support.intrinsicScale nu cstar gamma t ≤ r) : (r / Support.intrinsicScale nu cstar gamma t) ^ 2 ≤ min (r ^ 2 / (nu * t)) ((cstar⁻¹ * gamma) ^ (1 / 2) * (r ^ (2 - gamma) / t) ^ (1 - gamma)⁻¹)