DirichletLowerBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the Dirichlet lower bound of the corrector-limit proof #
ABK26, Lemma l.corrector.limit, Step 2, proves
liminf_{K→∞} E[ ‖∇w_D^{(K)}‖²_{L²(cu_K)} ] ≥ E[|∇w|²],
the display e.lower.bound.corrector.limit.
This file proves that display. The only non-elementary input is part (i) of
l.approximation.stationary.by.local, which is available here unconditionally
as
exists_isPotentialZeroTraceOn_limsup_le_of_mem_stationaryPotentialSubspace,
so the results below are not conditional on the approximation lemma: they
consume the proved form of it.
The route differs from the manuscript's in one respect, recorded here. The
paper reorganizes the three testing identities of
e.testing.by.vKL.corrector.limit and then applies Hölder to the resulting
cross term. We instead use the variational form of the same step:
∇w_D^{(K)} minimizes E_K over H¹₀(cu_K), so testing against the local
competitor ∇v_{K,L} gives, after completing the square,
⨍|∇w_D^{(K)}|² ≥ ⨍|f|² - ⨍|∇v_{K,L} + f|²
(Algsuperdiff/Section3/Provider/Corrector/CubeComparison.lean). The
right-hand side is then controlled by a pointwise Young split against the
stationary flux j = f + ∇w, which avoids any Cauchy-Schwarz inequality on the
product Ω × cu_K — a step that is not available here, because part (i)
supplies its competitor family with per-sample regularity only and no joint
measurability. The two routes give the same conclusion; ours needs strictly
less measure theory.
Disclosure. Nothing in this file realizes the source node
l.corrector.limit. Step 3 of the manuscript proof, the Neumann upper bound
e.upper.bound.neumann.corrector.limit, consumes part (ii) of
l.approximation.stationary.by.local — the local solenoidal approximation
built from the JKO94 Chapter-7 stream potential of a stationary solenoidal
field — and no form of that input exists in this repository. Without it the
sandwich of Step 4 cannot be closed, so only the lower half of
e.corrector.limit is proved here.
Elementary carrier bridges #
The squared Euclidean norm of a promoted vector is its dot square.
Forgetting the Hilbert structure preserves square integrability.
Promoting a plain vector field preserves square integrability.
Square integrability of a zero-trace potential field.
The normalized L² norm of a square-integrable field is the cube average of
its squared pointwise norm. This is the computation used inside
Algsuperdiff.Section3.Provider.Corrector.integral_cubeLpNorm_two_rpow_realize,
isolated for reuse.
The per-sample Young split of the competitor flux #
Promotion to the Euclidean Hilbert carrier is additive.
The competitor flux decomposes as the realized stationary flux plus the
approximation error: ∇v_{K,L} + f = (∇w + f) + (∇v_{K,L} - ∇w), pointwise in
space and in the sample.
The Step-2 comparison after the Young split, at a fixed sample.
For a Dirichlet gradient D on the cube, a zero-trace competitor v, and every
δ > 0,
⨍|f|² - (1+δ) ⨍|∇w + f|² - (1+δ⁻¹) ⨍|v - ∇w|² ≤ ⨍|D|²,
where all fields are the spatial realizations at the sample ω. This is the
manuscript's Step 2 with the Hölder step replaced by a pointwise Young
inequality; see the module docstring.
The expected lower bound at a fixed scale #
The expected Step-2 comparison at a fixed cube. Integrating
cubeAverage_vecDot_self_ge_young over the sample space and applying the
stationary transfer turns the two realized cube averages into the expectations
E[|f|²] and E[|∇w + f|²].
The corrector-limit lower bound #
The localization error C 3^{-L} of part (i) of
l.approximation.stationary.by.local can be driven below any positive
threshold by taking L large.
e.lower.bound.corrector.limit, in the ε-form.
Let f be a stationary square-integrable forcing and let ∇w = p be the
whole-space stationary corrector gradient of l.corrector.limit, i.e. the
element of L²(Ω;ℝᵈ) characterized by ∇w ∈ L²_pot(Ω) (hpmem) and f + ∇w ∈ L²_sol(Ω) (hflux), which is the weak form of -Δw = ∇·f on ℝᵈ. Let
∇w_D^{(K)} = Dfam K be the Dirichlet gradients of e.corrector.limit.pde.
Then for every ε > 0, eventually in K,
E[|∇w|²] - ε ≤ E[ ‖∇w_D^{(K)}‖²_{L²(cu_K)} ].
The proof consumes part (i) of l.approximation.stationary.by.local in the
form exists_family_bound, the Step-2 comparison of
Algsuperdiff/Section3/Provider/Corrector/CubeComparison.lean, and the
stationary transfer.
Disclosure. This is the lower half of e.corrector.limit only. It is not
the source node l.corrector.limit and claims no node status; the matching
Neumann upper bound needs part (ii) of the approximation lemma, which does not
exist in this repository.