StationaryCarrierTransport #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Transporting the stationary potential projection along an equivariant factor map #

Two stationary carriers can present the same random field. In this repository the fresh-shell forcing is read both on CoarseGraining's regular-field carrier RegCoeffField d — where the frozen assumption (J4) states the corrector energy — and on the continuous-path carrier C(Vec d, Mat d) — where the corrector limit l.corrector.limit is proved, because that carrier alone supports the joint measurability of the translation action. The two stationary L² layers sit over different σ-algebras, so the two canonical Helmholtz correctors are a priori unrelated.

This file supplies the missing comparison in complete generality. Let Φ : Ω₂ → Ω₁ be measurable, equivariant for the two real translation actions, and push the second law forward to the first. Write

carrierTransport E hΦ : L²(Ω₁) →L L²(Ω₂) for the Koopman isometry u ↦ u ∘ Φ;
carrierTransportAdj E hΦ for its Hilbert adjoint.

Both maps intertwine the two Koopman families — the transport by construction, its adjoint by taking adjoints in the intertwining relation and using the proved Koopman adjoint identity inner_koopman_left of Algsuperdiff/Section3/Provider/Corrector/MollifiedDecorrelation.lean. Consequently both map horizontal gradients to horizontal gradients, hence both map stationary potential subspace into stationary potential subspace (mem_stationaryPotentialSubspace_carrierTransport and mem_stationaryPotentialSubspace_carrierTransportAdj). That two-sided invariance is exactly what makes the two orthogonal projections correspond:

stationaryPotentialProjection (carrierTransport F) = carrierTransport (stationaryPotentialProjection F),

and therefore the two projected energies agree (norm_stationaryPotentialProjection_carrierTransport).

No identification of the two σ-algebras is used, and the transport is not assumed surjective: the adjoint direction replaces both.

Main results #

hasHorizontalGradient_of_intertwine — a bounded pair of maps intertwining the translation actions and compatible with coordinates carries horizontal gradients to horizontal gradients.
stationaryPotentialProjection_carrierTransport — the projections correspond.
norm_stationaryPotentialProjection_carrierTransport — the projected energies agree.

Disclosure. Nothing in this file realizes any source node: it is a Hilbert-space comparison of two carrier presentations of one stationary field. It consumes only Mathlib, Algsuperdiff.Probability.StationaryProjection and the Koopman algebra of MollifiedDecorrelation.lean. No draft theorem, in particular not Frozen.External.calderon_zygmund, is used.

StationaryCarrierTransport #

Transporting the stationary potential projection along an equivariant factor map #

Main results #

Intertwining maps preserve horizontal gradients #

The transport along an equivariant factor map, and its adjoint #

Both directions preserve the stationary potential subspace #

The two stationary potential projections correspond #