GeneratorRenormalization #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Generator renormalization for the coefficient field — [ABK] Theorem B #
Source: algsuperdiff.tex of arXiv:2601.22142v2, Theorem B of the introduction
(t.homogenization).
At every scale m the coarse-grained generator of the coefficient field
a = nu I + k is a constant multiple sigmaBar of the identity,
quantitatively close to sqrt (nu^2 + cstar gamma^{-1} 3^{2 gamma m}), and
the disorder solution u is compared with the homogenized solution v of the
same Dirichlet problem: a single random error amplitude with Gaussian-type
moments controls both the uniform difference u - v and the difference of the
two Dirichlet energies.
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 two Dirichlet problems 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.generator_renormalization 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 comparison holds for almost every sample under
fullSampleLaw M, with a single exceptional set serving the whole family of data at the scalem: the quantifiers overu,v,h,gand the three constants sit inside the almost-sure clause. The moment bound on the error amplitude is a separate, annealed clause. - The diffusivity.
sigmaBarMis existential, as the printed statement has it: "there exist an effective diffusivity and a random variable". It is not tied to a name here, and it may depend onm. - Moments. The bound on
E_Bis stated as∫⁻ E_B^p ≤ (ENNReal.ofReal B)^prather than through thep-th root of the integral. The two are equivalent for a nonnegative bound, and the power form is the one anℝ≥0∞-valued integral states without a division; it also needs no integrability or measurability premise, which the printed estimate does not have either. - 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)}, and it appears here asKhInf + 3^{m/2} Kh:KhInfbounds‖h.grad x‖in the sup norm over the open cube andKhbounds its1/2-Hölder seminorm. 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 two conclusions. The uniform estimate is written as an
almost-everywhere pointwise bound of
3^{-m} |u - v|against the volume measure restricted to the open cube, which is the essential supremum of the source read without a supremum. The energy estimate compares the volume averages ofnu |∇u|²and ofsigmaBarM |∇v|²over the same cube. - Constants.
gamma0andCare chosen before the model 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 diffusivity comparison, the moment amplitude and the upper end of the range ofp, 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.