PointwiseDecay

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

Pointwise exponential decay away from the transition layer

This module assembles the exponentially weighted mass estimate, the conversion of that estimate into a local L² bound, and the interior pointwise estimate into a single statement: a bounded solution decays exponentially away from the region where the localization is not yet constant, at the rate

kappa * alpha / (alpha + d / 2),

where kappa is any rate admissible for the weighted estimate, in particular sqrt (lam * mass) / (2 * sqrt 2 * Lam).

The geometry enters only through four checkable conditions: the localization is one near the point, the phase is at least tx near the point, the phase is at most tA wherever the localization is not locally constant, and tA <= tx.

What the estimate costs, stated plainly. The dimension satisfies 2 <= d; d = 1 is excluded, because the interior Hölder modulus comes from the Schauder estimate on balls, which is stated for 2 <= d. The radius r of that ball is arbitrary: any 0 < r with euclideanBall x r inside the domain will do, and the constant carries the explicit powers of r, so the estimate may be applied at a small scale near the boundary. The localization and phase conditions are read on euclideanBall x (r / 2), the largest radius the balance uses. The Hölder exponent satisfies alpha in [1/2, 1), and the coefficient field is within smallContrastThreshold d alpha of the identity. The constant is a sum of two terms, not a single multiple of the uniform bound: the weighted L² term, carrying M, the layer constant Ceta and the measure volLayer of the transition layer, plus an additive Schauder summand built from the local gradient size E and the forcing bound G; both are multiplied by the exponential factor. Finally the conclusion is a per-point existential: some function continuous on euclideanBall x (r / 2) and almost everywhere equal to the solution on euclideanBall x r is small at x. Decay/Representative.lean transfers that bound to any fixed continuous representative.

Main results

• DivergenceFormProcess.Decay.fderiv_eq_zero_of_eventuallyEq_one

noncomputable def DivergenceFormProcess.Decay.agmonRate (lam Lam mass : ℝ) : ℝ

The admissible Agmon rate: the largest kappa allowed by the absorption condition 8 Lam ^ 2 kappa ^ 2 <= lam * mass.

Equations

• DivergenceFormProcess.Decay.agmonRate lam Lam mass = √(lam * mass) / (2 * √2 * Lam)

theorem DivergenceFormProcess.Decay.agmonRate_nonneg {lam Lam mass : ℝ} (hLam : 0 < Lam) : 0 ≤ agmonRate lam Lam mass

theorem DivergenceFormProcess.Decay.agmonRate_admissible' {lam Lam mass : ℝ} (hlam : 0 ≤ lam) (hmass : 0 ≤ mass) (hLam : 0 < Lam) : 8 * Lam ^ 2 * agmonRate lam Lam mass ^ 2 ≤ lam * mass

theorem DivergenceFormProcess.Decay.fderiv_eq_zero_of_eventuallyEq_one {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {W : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hf : ∀ y ∈ W, f y = 1) {x : HCPolySupport.Vec d} (hx : x ∈ W) : fderiv ℝ f x = 0

A function equal to one on a neighbourhood has vanishing derivative.