AnomalousRegularityLimit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Anomalous regularity for the stream coefficient field #
The excess-decay estimate of the anomalous regularity theorem is available for
the truncated coefficient fields a_L = nu I + k_L, uniformly in the truncation
scale L above the cube scale m, on the cutoff sample space. This file
carries it to the full stream field a = nu I + k on the full-sample carrier,
by the limit L -> infinity.
Two mechanisms are combined.
The probabilistic half is a transport along
Subtype.val: the law of the full-sample carrier pushes forward to the cutoff-sample law, so the minimal scale, its tail bound and the almost-sure clause move to the new carrier with no loss. The minimal scale is the same random variable, read along the inclusion; in particular the estimate for the truncated fields is available at every truncation scale with one and the same exceptional set.The analytic half is the closedness of the display under
L^2convergence of the gradients. For a datumhand a forcegfixed once and for all, the Dirichlet problem fora_Lis solvable on the cube for everyL, and the gradients of its solutions converge inL^2to the gradient of the given solution fora. Each of the two inequalities of the display is a bound between twoL^2magnitudes of the gradient against normalized window measures, and the reverse triangle inequality bounds the defect of each side by theL^2norm of the gradient difference over the window, at the cost of the inverse square root of the window's volume. Both windows have positive volume, so those amplitudes are finite, the defects vanish along the limit, and the inequality passes to it.
Main results #
sqrt_vecNormSq_le_sqrt_card_mul_norm,continuous_sqrt_vecNormSq— the Euclidean magnitude against the ambient sup norm.eLpNorm_sqrt_vecNormSq_normalized_le,eLpNorm_sqrt_vecNormSq_restrict_le— the twoL^2atoms for the normalized window measure.excess_display_closed— the closedness of the display underL^2convergence of the gradients.exists_isDirichletSolutionOn_cutoff— the truncated Dirichlet problems with the given datum and force.tendsto_sqrt_integral_grad_sub— the gradients of the truncated solutions converge inL^2to the gradient of the full-field solution.anomalous_regularity_provider— the anomalous regularity estimate for the stream coefficient field.
References #
- ABK26, Theorem C and the passage from the truncated fields
a_Ltoa.
1. The Euclidean magnitude against the ambient norm #
The squared Euclidean magnitude is continuous on Vec d.
The Euclidean magnitude is continuous on Vec d.
sqrt (sum x i ^ 2) <= sqrt d * sup |x i|. Vec d carries the product
norm; the display of the regularity theorem is written in the Euclidean
magnitude. This is the only constant the comparison of the two costs.
The Euclidean magnitude of a square-integrable field is almost everywhere strongly measurable on the domain.
The Euclidean magnitude of a square-integrable field is almost everywhere strongly measurable against the normalized measure of any subwindow.
2. Two L² atoms for the normalized window measure #
The window move to the ambient domain. The normalized L² magnitude
over a subwindow is the plain L² magnitude over the domain, at the cost of the
inverse square root of the window's volume.
The dictionary with the energy integral. The L² norm of the Euclidean
magnitude of a square-integrable field over the domain is bounded by sqrt d
times the square root of the energy of the field in the ambient norm.
The triangle inequality for the L² magnitude of a field.
The Euclidean magnitude of a difference is symmetric in its two arguments.
3. The limit passage in ℝ≥0∞ #
A two-sided inequality with vanishing defects passes to the limit. If
a is below a family PA up to a defect, the family PW is above b up to a
defect, the two families satisfy PA ≤ K (PW + c) eventually, and both defects
are a finite multiple of a real quantity tending to zero, then a ≤ K (b + c).
4. Closedness of the excess-decay display #
The excess-decay display is closed under L² convergence of the fields.
If the display holds for a family of fields G L on a subwindow A of a domain
W, both of positive volume, and G L converges to F in L² on W, then it
holds for F with the same constants.
5. The truncated Dirichlet problems with the given data #
The truncated Dirichlet problem on the origin cube is solvable with the
given datum and force. The truncated field is elliptic on the cube and the
force is square integrable, so the Lax-Milgram construction supplies a solution
of the form h + w with w of zero trace.
The gradients of the truncated solutions converge in L², on a cube
centred anywhere, to the gradient of the full-field solution of the same
Dirichlet problem. Two solutions of the same problem for two coefficient fields
differ by a zero-trace function whose energy is bounded by the supremum distance
of the two fields times the energy of one solution, and that distance is
geometric in the truncation scale.
The L² convergence of the gradients of the truncated solutions, read on
the origin cube.
6. The transports along the inclusion of the full-sample carrier #
Events of the cutoff sample space transport to the full-sample carrier.
The tail events of an ℕ∞-valued random variable transport to the
full-sample carrier.
Almost-sure clauses of the cutoff sample space transport to the full-sample carrier.
7. Anomalous regularity for the stream coefficient field #
Anomalous regularity for the stream coefficient field. For a disorder
model of small enough strength, and every Hölder exponent below
1 - C sqrt gamma, there is an almost surely finite minimal scale with an
exponential tail such that, above it, every Dirichlet solution of the field
nu I + k on a triadic cube with C^{0,1/2} force and C^{1,1/2} boundary
datum satisfies the large-scale excess decay 3^{(1-alpha)(m-n)} between any
two scales n ≤ m.