Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.DivergenceForm.Decay.Tail

Tail #

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

The explicit resolvent tail function #

Let z solve mu z - div (a grad z) = g on an open bounded domain Om with zero trace, let x be a point of Om and r > 0 a radius with euclideanBall x r inside Om, and let the source g vanish almost everywhere on that ball. With the maximum-principle bound |z| <= 1 / mu, the value of mu * z at x decays in the dimensionless variable

s = sqrt mu * r,

and this file makes that decay explicit: agmonTailFunction d lam Lam alpha is a closed-form function of s alone, with constants depending only on the dimension d, the two ellipticity constants lam and Lam, and the Hölder exponent alpha.

The hypotheses that restrict the estimate. The dimension satisfies 2 <= d, the Hölder exponent lies in Set.Ico (1 / 2) 1, and the coefficient field is not merely uniformly elliptic with constants lam and Lam: it is required to be within small contrast of the identity, that is CoefficientIdentityDistanceLE Om a delta for some delta <= smallContrastThreshold d alpha. The small-contrast hypothesis is what supplies the interior Schauder estimate behind the gradient and the forcing terms, and it is the reason the chain does not apply to a merely uniformly elliptic field. Subject to those hypotheses the right-hand side is free of the domain, the coefficient field, the source and the solution.

Why s is the only variable. The equation is scale invariant, and mu r ^ 2 is the only dimensionless combination of the mass and the radius, so every term of the pointwise constant must be a function of s after multiplication by mu. Each of the three terms is checked against that requirement: the weighted L² term carries M <= 1 / mu from the maximum principle, the layer gradient bound Ceta which scales like r ^ (-2), and the layer volume volLayer which scales like r ^ d, and it contributes s ^ (-1); the Schauder gradient term carries the Caccioppoli gradient size, itself proportional to 1 / mu times r ^ ((d - 2) / 2), and contributes a constant; the Schauder forcing term carries the forcing bound one and contributes s ^ 2. Nothing else survives.

The geometry. The localization is one on the ball of radius 3 r / 4 and vanishes outside the ball of radius r, so its transition layer sits where the source vanishes; the phase is the inward radial phase about x with regularization r / 8; the interior estimate is applied on the ball of radius r / 2. The point is then at phase -(r / 4) and the layer at phase -(3 r / 4) + r / 8, a gap of 3 r / 8.

The exponential domination agmonTailFunction_le_exp is what a consumer of the tail estimate needs: beyond s = 1 the tail function is at most agmonTailDominationConstant d lam Lam alpha times exp (-(agmonTailRate d lam Lam alpha / 2) * s).

The bound does not mention the domain except through the containment of the ball.

Main results #

The tail function #

source
noncomputable def DivergenceFormProcess.Decay.agmonTailL2Coefficient (d : ℕ) (lam Lam : ℝ) :
ℝ

The coefficient of the s⁻¹ term of the tail function: the weighted L² term of the pointwise estimate, after the mass mu and the radius r have been absorbed into s = sqrt mu * r.

Equations
Instances For
    source
    noncomputable def DivergenceFormProcess.Decay.agmonTailGradientCoefficient (d : ℕ) (lam Lam alpha : ℝ) :
    ℝ

    The constant term of the tail function: the Schauder gradient term of the pointwise estimate, whose local gradient size is supplied by the Caccioppoli bound. It carries no power of s at all.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def DivergenceFormProcess.Decay.agmonTailForcingCoefficient (d : ℕ) (alpha : ℝ) :
      ℝ

      The coefficient of the s ^ 2 term of the tail function: the Schauder forcing term of the pointwise estimate, whose forcing bound is one.

      Equations
      Instances For
        source
        noncomputable def DivergenceFormProcess.Decay.agmonTailRate (d : ℕ) (lam Lam alpha : ℝ) :
        ℝ

        The decay rate of the tail function in s = sqrt mu * r: the Agmon rate sqrt (lam * mu) / (2 sqrt 2 * Lam) reduced by the Hölder exponent factor alpha / (alpha + d / 2) and read across the gap 3 r / 8 between the point and the transition layer of the localization.

        Equations
        Instances For

          Signs #

          source
          theorem DivergenceFormProcess.Decay.agmonTailL2Coefficient_nonneg (d : ℕ) {lam Lam : ℝ} (hLam : 0 ≤ Lam) :
          0 ≤ agmonTailL2Coefficient d lam Lam

          The s⁻¹ coefficient is nonnegative.

          source
          theorem DivergenceFormProcess.Decay.agmonTailGradientCoefficient_nonneg (d : ℕ) {lam Lam alpha : ℝ} (hlam : 0 < lam) (hLam : 0 ≤ Lam) :
          0 ≤ agmonTailGradientCoefficient d lam Lam alpha

          The constant coefficient is nonnegative.

          source
          theorem DivergenceFormProcess.Decay.agmonTailForcingCoefficient_nonneg (d : ℕ) (alpha : ℝ) :
          0 ≤ agmonTailForcingCoefficient d alpha

          The s ^ 2 coefficient is nonnegative.

          source
          theorem DivergenceFormProcess.Decay.agmonTailRate_pos (d : ℕ) {lam Lam alpha : ℝ} (hlam : 0 < lam) (hLam : 0 < Lam) (halpha : 0 < alpha) :
          0 < agmonTailRate d lam Lam alpha

          The tail rate is positive.

          The frozen scale identification #

          source
          noncomputable def DivergenceFormProcess.Decay.agmonFrozenDecayConstant (d : ℕ) (D alpha E G r₀ : ℝ) :
          ℝ

          The pointwise constant before its dimensional variables are collected.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem DivergenceFormProcess.Decay.mul_agmonDecayConstant_frozen_eq {d : ℕ} [NeZero d] {lam Lam nu mu r r₀ alpha : ℝ} (hlam : 0 < lam) (hLam : 0 < Lam) (hmu : 0 < mu) (hr : 0 < r) (hr₀ : 0 < r₀) :
            mu * agmonFrozenDecayConstant d (1 / mu * √(8 * Lam ^ 2 / (lam * mu) * agmonTailCutoffGradientBound d r * agmonTailLayerVolume d r)) alpha (agmonTailGradientSize d lam Lam mu r) (1 / nu) r₀ = agmonTailL2Coefficient d lam Lam / (√mu * r) * (√mu * r / (2 * (√mu * r₀))) ^ (↑d / 2) + agmonTailGradientCoefficient d lam Lam alpha * (√mu * r / (2 * (√mu * r₀))) ^ (↑d / 2 - 1) + 4 * agmonTailForcingCoefficient d alpha * (√mu * r₀) ^ 2 / nu

            Scale identification for the frozen pointwise constant.

            The scale-free identification of the pointwise constant #

            source
            theorem DivergenceFormProcess.Decay.agmonRate_mul_eq (d : ℕ) {lam Lam mu r alpha : ℝ} (hlam : 0 < lam) :
            agmonRate lam Lam mu * alpha / (alpha + ↑d / 2) * (3 * r / 8) = agmonTailRate d lam Lam alpha * (√mu * r)

            The exponent of the pointwise estimate, read across the gap 3 r / 8, is the tail rate evaluated at s = sqrt mu * r.