SuperdiffusivityV2 #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Quenched power-law superdiffusivity — [ABK] Theorem A #
Source: references/algsuperdiff.tex:145-183.
Let nu, gamma and cstar be positive and, for a time t > 0, let
R(t) = ((nu t)^{2-gamma} + cstar gamma⁻¹ t²)^{1/(2(2-gamma))}
be the intrinsic length scale of the model at that time. For a disorder model
of strength gamma small enough there are constants gamma0 and C,
depending only on the dimension and on the value cstar of the model's
nondegeneracy constant, such that for every moment
p ∈ [1, C⁻¹ gamma⁻¹ |log gamma|⁻⁶] the diffusion generated by
∇·(nu I + k)∇ started at the origin satisfies two estimates: its mean square
displacement at time t is within
C (p^{1/2} + |log gamma|^{1/2}) gamma^{1/2} |log gamma|⁴ R(t)² of 2 d R(t)²,
and its mean displacement has square at most
C (p + |log gamma|) gamma |log gamma|⁷ R(t)², both as Lᵖ-norm bounds over
the disorder. Equivalently, the raw p-th moments are bounded by the
respective amplitudes raised to p. The first estimate is the quantitative statement that the
particle spreads like R(t), which is superdiffusive above the crossover time;
the second controls its quenched mean displacement.
The process #
The realization of the environment is a sample omega of the model's field,
and streamExhaustionTailInput M omega carries the data from which the
continuous-path process of that realization is built. Its wholeSpaceProcess
is the unique Markov kernel on continuous paths whose finite-dimensional
distributions are those of the semigroup represented by the resolvent of
nu I + k_omega, so the two estimates speak about that one process and about
nothing carried by the construction data.
The two objects the displays name #
- The displacement is read through
onePointRetract (0 : Vec d), the retraction of the one-point compactification ofVec dontoVec dthat sends the added point to the origin. It agrees pointwise with the plainfun z => Option.getD z 0, and it is the function the measurability statements of the quenched expectations are proved against. - The length scale
R(t)isintrinsicScale M.nu cstar M.gamma t, the displayed formula above with its arguments in the ordernu cstar gamma t.
Reading of the statement #
- State space. The process is built on the one-point compactification of
Vec d. Two consequences are visible in the statement. The starting point is written as the image of(0 : Vec d)in the compactification, since the compactification carries no numeral of its own. The displacement is read through the retraction just described; the value it assigns at the added point is invisible, because a process started at a live point almost surely never reaches that point. - Path space and its metric. The two
letIlines supply the metric on the compactification in which the paths are continuous, and its completeness. They are the same two the process itself carries in its type, and they fix the Borel structure the two integrals are taken against. - Annealed form. Both estimates are
L^pnorms over the disorder, so the environment is integrated, not quantified: there is no almost-sure clause, and none is printed. The outer expectation is anℝ≥0∞-valued integral over the carrier of the field under its law, and the inner quenched expectation is a Bochner integral against the law of the process. p-th-power form. Each estimate is stated as∫⁻ Z^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 to be well-defined. The displayed inequalities alone do not establish integrability of the inner observables: a nonintegrable Bochner integrand has integral zero in Lean. The Theorem A import therefore includes public companion theorems:Algsuperdiff.Section5.Provider.exists_ae_integrable_streamProcess_displacementproves almost-everywhere integrability of both observables at sufficiently small coupling, andAlgsuperdiff.Section5.Measurability.measurable_streamProcess_displacement_expectationsproves measurability of their quenched expectations.- Time range. The time is any positive real. The crossover time appears in the discussion following the printed theorem, never as a hypothesis.
- Constants.
gamma0andCare chosen before the model and before the time, so they depend only ondand oncstar, which is the printed dependence; in particular they do not depend onnu. OneCserves both amplitudes and the upper end of the range ofp, as printed. - Carrier. The disorder is integrated over 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, its resolvent and its process total functions of the sample rather than partially defined ones.
- Non-vacuity. The carrier is inhabited for every model, since its law is a
probability measure. This is a conditional theorem for models satisfying
the stated assumptions. The development does not construct a concrete
ABKModel dor prove non-emptiness of that model class.
Where the two amplitudes come from #
The proof reaches each display through a product of two factors. The first is
the moment of the renormalization error of Theorem B evaluated at the random
scale m_t at which the particle is confined up to time t; the second is the
moment of 3^{2 m_t} itself. Normalizing m_t by its deterministic lower
bound makes the random part of the first factor free, so it is the Theorem B
amplitude C (p^{1/2} + |log gamma|^{1/2}) gamma^{1/2} |log gamma|³, and the
second factor is C |log gamma| R(t)². Their product is the amplitude of the
first display, C (p^{1/2} + |log gamma|^{1/2}) gamma^{1/2} |log gamma|⁴ R(t)²,
and squaring the p-dependent factor gives the second display,
C (p + |log gamma|) gamma |log gamma|⁷ R(t)², both as in the paper.
The confinement scale is chosen at least of order
|log gamma|^{1/2} R(t). The exit-time estimate at that scale makes the
stopping-removal error polynomially small in gamma.
Conventions #
- The displayed quantity is the summed
2 d R(t)², as in the paper. The proposition the proof reaches is the per-direction form with2 R(t)², and the two are joined by summing over the standard basis: the squared Euclidean length is the sum of the squared coordinates. - The two amplitudes carry the factors
p^{1/2} + |log gamma|^{1/2}andp + |log gamma|, as in the paper. They are the factors the renormalization theorem supplies and this proof consumes down top = 1; forpof order|log gamma|and above they agree withp^{1/2}andpup to a constant.
Proved; reduces to the standard axioms.