LocalizedBoundaryAsymptotics #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The elementary asymptotic behind localized conservativity #
An exponential in the inward triadic distance dominates both the
volume-order prefactor and one logarithmic loss in the localized decay rate.
The proof compares everything with (sqrt 3)^m and keeps exp opaque.
theorem
DivergenceFormProcess.Form.tendsto_triadicVolume_mul_exp_neg_triadic_div_linear
(d : ℕ)
{C c : ℝ}
(hC : 0 ≤ C)
(hc : 0 < c)
:
A volume-order geometric prefactor times an exponential with one linear loss in the exponent tends to zero along the triadic exhaustion.