StationaryCorrector #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the whole-space stationary corrector as a critical gradient field #
ABK26, Lemma l.corrector.limit,
introduces w, "the unique (up to constants) solution of -Δw = ∇ · f in ℝᵈ
with ∇w ∈ L²_pot stationary". In the Hilbert-space realization
of Algsuperdiff/Probability/StationaryProjection.lean this determines ∇w
exactly: ∇w lies in stationaryPotentialSubspace and ∇w + f is orthogonal
to it, i.e. ∇w + f ∈ stationarySolenoidalSubspace; equivalently
∇w = -stationaryPotentialProjection f. This is the same construction and the
same sign convention already used by
Algsuperdiff/Probability/StationaryValueProjection.lean for the J4 corrector
zeroShellPotentialCorrector, but stated for a general translation-invariant
carrier rather than the shell-model one.
This file records the facts about that object that the corrector-limit proof
uses at the level of the probability Hilbert space, in particular the display
e.pot.sol.decomposition.corrector.limit
E[f · ∇w] = -E[|∇w|²].
Everything is obtained by specializing the carrier-free lemmas of
Algsuperdiff/Section3/Provider/Corrector/VariationalEnergy.lean to
V = stationaryPotentialSubspace; no per-realization (spatial) information is
used or produced here.
Stationary potential fields are orthogonal to stationary solenoidal fields.
This is the Hilbert-space content of ∫ p · j = 0 for p ∈ L²_pot,
j ∈ L²_sol.