PotentialApproximation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the potential half of the local-approximation lemma #
This file proves the cutoff core of part (i) of
l.approximation.stationary.by.local:
(i) Potential approximation. For every
L ∈ ℕthere exists a family >{v_{K,L}}_{K ∈ ℕ}withv_{K,L} ∈ H¹₀(cu_K)such that >limsup_{K→∞} E[ ‖∇v_{K,L} − p‖²_{L²(cu_K)} ] ≤^{−L} E[|p|²].
The paper's proof fixes η_{K,L} ∈ C_c^∞(cu_K) equal to 1 away from a
boundary strip of relative width 3^{−L} and with |∇η_{K,L}| ≤^{L−K}, takes
a spatial primitive φ of p and sets v_{K,L} := η_{K,L}(φ − (φ)_{cu_K}).
The error splits as ∇v_{K,L} − p = (η_{K,L} − 1) p + (φ − (φ)_{cu_K}) ∇η_{K,L}, the first term being controlled by the strip volume
e.boundary.strip.volume and the second by the sublinearity of φ.
Here the primitive is taken from the stationary L² layer: φ is a
square-integrable random variable whose spatial realization is a smooth
primitive of the realization of p. For such a primitive no mean subtraction
and no sublinearity input is needed: the second error term is bounded by
‖∇η_{K,L}‖²_∞ E[φ²] ≍ 3^{2(L−K)} E[φ²], which already tends to 0 as K → ∞
at fixed L because E[φ²] is finite.
The cutoff is CoarseGraining's
Homogenization.QuantitativeCubeCutoff.canonical at the concentric ratios ρ₁ = 1 − 3^{−L}/2 and ρ₂ = 1 − 3^{−L}/4; the strip fraction 1 − ρ₁ ^ d ≤ d · 3^{−L}/2 comes from
Algsuperdiff/Section3/Provider/Corrector/BoundaryStrip.lean, so the paper's
C is chosen explicitly as C = d (design decision D-6).
The concentric ratios of the paper's cutoff #
Inner concentric ratio of the localization cutoff at scale L: the cutoff
equals 1 on the subcube of relative radius 1 − 3^{−L}/2.
Instances For
Outer concentric ratio of the localization cutoff at scale L: the cutoff
is supported in the subcube of relative radius 1 − 3^{−L}/4.
Instances For
e.boundary.strip.volume, scalar half at the chosen ratios. The strip
fraction of the localization cutoff at scale L in dimension d is at most
d · 3^{−L} / 2.
The cutoff and its gradient bound #
The paper's cutoff η_{K,L}, defined as CoarseGraining's canonical
quantitative cube cutoff between the concentric ratios cutoffInnerRatio L and
cutoffOuterRatio L.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The uniform gradient bound of the localization cutoff, C(d) 3^{L−K} in the
notation of the paper.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gradient of the localization cutoff, as a Euclidean vector.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gradient bound of the localization cutoff on the origin cube of scale
K, in the paper's explicit form C(d) 3^{L−K}.
The local approximant and its error #
The gradient of the paper's local test field
v_{K,L} = η_{K,L} · φ, written out by the product rule. It is defined by this
formula for every sample, so that it is jointly measurable without any
smoothness assumption; whenever the realization of φ really is a smooth
primitive of the realization of p it is the gradient of an H¹₀(cu_K)
function (isPotentialZeroTraceOn_localGradApprox).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The approximation error ∇v_{K,L} − p, decomposed exactly as in ABK26.
The local test field is an honest zero-trace potential on the cube, i.e.
v_{K,L} ∈ H¹₀(cu_K) in the notation of the paper.
Pointwise error bound. On the cube the local approximation error is controlled by the boundary strip and by the primitive, exactly as in the two displays of ABK26.
The expected error at a fixed cube #
The boundary strip Σ_{K,L} of ABK26: the part of the cube on which the
localization cutoff may differ from 1.
Equations
Instances For
e.boundary.strip.volume. The strip volume is at most
d · 3^{−L} / 2 times the volume of the cube
(ABK26, with the explicit constant C = d
of design decision D-6).
The expected squared error over a fixed cube, before normalization.
The approximation error is a strongly measurable field for every sample.