AnomalousRegularity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Anomalous regularity for the coefficient field — [ABK] Theorem C #
Source: algsuperdiff.tex of arXiv:2601.22142v2, Theorem C of the introduction (t.regularity).
For a disorder model of strength gamma small enough, and every Hölder
exponent alpha below 1 - C sqrt gamma, there is an almost surely finite
minimal scale X with an exponential tail such that, above X, every
Dirichlet solution of the coefficient field nu I + k on a triadic cube with
C^{0,1/2} force g and C^{1,1/2} boundary datum h satisfies the
C^{0,alpha} large-scale excess decay 3^{(1-alpha)(m-n)} between any two
scales n ≤ m.
The carrier and the coefficient field #
The disorder is read on Algsuperdiff.Section5.Field.FullSample d M.gamma
under Algsuperdiff.Section5.Field.fullSampleLaw M, the carrier the quenched
superdiffusivity estimates use: the subtype of samples on which the field's
two-sided scale rates and gradient bounds hold. That event has full measure
for the unrestricted law, so the restriction loses nothing, and it is what
makes the coefficient field a total function of the sample rather than a
partially defined one.
The field is Algsuperdiff.Section5.Field.streamCoefficient M.nu omega, that
is nu I + k_omega with k_omega x = Σ_{n ∈ ℤ} (j_n x - j_n 0). The shell
sum is normalized at the origin, which fixes the additive constant the source
leaves free. The choice is invisible to the Dirichlet problem of the
statement: the shift is by a constant antisymmetric matrix, and
Algsuperdiff.Section4.Provider.ExcessDecay.isDirichletSolutionOn_sub_const_of_skew
says that such a shift moves no solution of the weak problem.
The form with an infrared cutoff #
Algsuperdiff.Frozen.Section4.anomalous_regularity asserts the same estimate
for the truncated field (coefficientCutoff nu L omega).toCoeffField,
uniformly in the cutoff L ≥ m, on the unrestricted sample space. That form
is the more general one and stays part of the public surface; the statement
here is the one the introduction prints, and follows from it in the limit
L → ∞. Outside the carrier, the law and the coefficient field the two
statements share every token.
Reading of the statement #
- Almost-sure form. The excess decay holds for almost every sample under
fullSampleLaw M, with a single exceptional set serving the whole family of data at the scalem. The tail bound on the minimal scale is a separate, annealed clause, and the same random variableXcarries both. - The minimal scale.
Xtakes values inℕ∞, so its type carries no finiteness assumption; the tail bound is what forces it to be almost surely finite. The scale clauseX omega ≤ (m - n).toNatis the printedX_m(alpha) ≤ m - nunder the hypothesisn ≤ m, where the truncated subtraction agrees with the integer one. - The diffusivity. The comparison amplitude is the named annealed gauge
Annealed.sigmaBar M m, not an existential: this theorem quotes the diffusivity that the renormalization theorem produces rather than producing one of its own. - The boundary datum. The normalized norm
3^{m/2} ‖∇h‖_{W^{1/2,∞}(□_m)}of the source is‖∇h‖_{L^∞(□_m)} + 3^{m/2} [∇h]_{C^{0,1/2}(□_m)}. A single constantKhbounds both pieces here — the sup norm ofh.gradby3^{m/2} Khand its1/2-Hölder seminorm byKh— so the printed sum is at most2 · 3^{m/2} Khand the factor2is absorbed intoC. The datum enters as anH1Functioncarrying a classical gradient, whichHasGradientOnpins toh.grad. - The force.
[g]_{W^{1/2,∞}(□_m)}is the1/2-Hölder seminorm boundKgon the open cube. - The indicator. The boundary-datum term of the printed display carries the
indicator of
x ∉ □_{m-1}. It appears here as a conjunction of two estimates: the one with that term, valid at everyxin the cube, and the one without it, valid whenx ∈ □_{m-1}. The two readings are equivalent. - The norms.
nu^{1/2} ‖∇u‖_{L²(S)}isENNReal.ofReal (sqrt nu)times theL²norm of|∇u|againstnormalizedVolumeMeasureOn S, the volume measure ofSnormalized to a probability measure, and the setsSare the intersections of the translated cubex + □_nwith□_m. - Constants.
gamma0andCare chosen before the model, before the exponent and before the scale, so they depend only on the dimensiondand on the valuecstarof the model's ellipticity parameter, which is the printed dependence. OneCserves the range ofalpha, the tail of the minimal scale and the amplitude of the excess decay, as printed. - Non-vacuity.
FullSample d M.gammais inhabited for every model, since its law is a probability measure. The model clause is another matter: this development constructs noABKModel d, so the clause is satisfiable only vacuously until a construction is supplied, exactly as for the other main statements of the development. The remedy is a separate construction theorem, not a change here.
Proved; reduces to the standard axioms.