TailFreezing

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

Resolvent tails from a frozen pointwise estimate

The Agmon energy estimate only uses uniform ellipticity. This module freezes the coefficient at the point where the final interior estimate is read. Thus the coefficient may have a continuous skew part of arbitrary size: small contrast is required only for the normalized frozen coefficient on the inner ball.

The two-scale tail function

noncomputable def DivergenceFormProcess.Decay.agmonTailFunctionFrozen (d : ℕ) (lam Lam nu alpha s s₀ : ℝ) : ℝ

The explicit two-scale tail function. Its arguments are s = sqrt mu * r and s₀ = sqrt mu * r₀, where r is the source-free radius and r₀ is the radius on which the normalized frozen coefficient has small contrast.

Equations

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