ValuePathTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Transporting the fresh-shell law to the continuous-path carrier #
The Ω-level decorrelation chain of
Algsuperdiff.Section3.Provider.Corrector.MollifiedDecorrelation needs three
structures on its carrier: MeasurableConstVAdd, MeasurableVAdd₂ and
VAddInvariantMeasure. On CoarseGraining's regular-coefficient carrier
RegCoeffField d the first and the third are available
(regCoeffFieldMeasurableConstVAdd and
Algsuperdiff.Section3.Provider.Corrector.vaddInvariantMeasure_zeroShellRegLaw),
but the second is not: CoarseGraining's carrier σ-algebra is generated by
pointwise evaluations and compactly supported entry tests of merely measurable,
locally integrable representatives, and joint measurability of (z, a) ↦ z +ᵥ a is not available there.
The continuous-path carrier C(Vec d, Mat d) does carry all three, by
Algsuperdiff.Assumptions.ShellField.TranslationAction
(valuePathMeasurableVAdd₂ and its parents). This file therefore transports
the fresh-shell law along ShellField.valuePath, transports the origin forcing
and its covariance kill, and instantiates the decorrelation chain there.
Main definitions #
zeroShellValuePathLaw— the pushforward of the zero-shell law alongShellField.valuePath, i.e. the law of the shell-zero values as a continuous matrix-valued path.valuePathForcing— the literal matrix-vector forcing at the spatial origin, read onC(Vec d, Mat d).valuePathForcingL2,valuePathPotentialCorrector— the forcing as an element of the stationaryL²layer, and the canonical source-sign potential correctorwof the Helmholtz splitting𝐣 = 𝐟 + ∇w, namely the negative of the orthogonal projection of the forcing onto the stationary potential subspace, built by the generic stationary projection ofAlgsuperdiff.Probability.StationaryProjectionat the transported carrier.
Main results #
zeroShellValuePathLaw_toMeasure_eq_map_valuePath,map_vadd_zeroShellValuePathLaw— the transported law is thevaluePathpushforward of the zero-shell law, and is unchanged by a real translation of the path.vaddInvariantMeasure_zeroShellValuePathLaw— the transported law is translation invariant, from the (J1) stationarity field alone.continuous_valuePathForcing,stronglyMeasurable_valuePathForcing,memLp_two_valuePathForcing— the transported forcing is continuous, hence strongly measurable, and square integrable through the (J2) Gaussian tail, which is what places it in the stationaryL²layer of the new carrier.
Nothing in the transport changes the mathematics: the transported forcing
composed with valuePath is literally (by rfl) the CoarseGraining origin
forcing composed with forgetShell, and both laws are pushforwards of one and
the same zero-shell law.
What is not transported #
The stationary L² layer of C(Vec d, Mat d) and the stationary L² layer of
RegCoeffField d sit over different σ-algebras, so the canonical corrector
built here is not identified with ShellField.zeroShellPotentialCorrector;
only the forcing, its covariance and its energy are shown to agree. Any
consumer that needs the CoarseGraining-carrier corrector must supply that
identification separately.
The energies of the two correctors are, however, equal, and that is proved
downstream in
Algsuperdiff/Section3/Provider/Corrector/FreshShellCorrectorEnergy.lean
(norm_valuePathPotentialCorrector_eq), by transporting the stationary
potential projection along the forgetful map regOfPath and its Hilbert
adjoint. A consumer that needs only the corrector energy — for instance to
read the frozen (J4) constant into the corrector limit — therefore needs no
further work; a consumer that needs the corrector element on CoarseGraining's
carrier still does.
Disclosure. Nothing in this file realizes any source node. It moves an
Ω-level provider chain to a carrier on which its structural hypotheses hold and
discharges its covariance hypothesis at the fresh shell; it does not prove part
(ii) of l.approximation.stationary.by.local and it claims no node status. In
integral_normSq_mollify_le_of_helmholtz_valuePath the Helmholtz data p, j
and their subspace memberships remain genuine binders, at the subspaces of the
transported carrier; they are discharged only for the canonical splitting built
below.
The fresh-shell law on the continuous-path carrier #
Reading the shell-zero coordinate and forgetting everything but its continuous matrix values is measurable.
The fresh-shell law on the continuous-path carrier. This is map (valuePath ∘ coord 0) P, the exact analogue of ShellField.zeroShellRegLaw
with CoarseGraining's regular-coefficient carrier replaced by the compact-open
carrier C(Vec d, Mat d).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The transported law is the valuePath pushforward of the zero-shell law.
The three structural instances at the new carrier #
Full real-translation invariance of the zero-shell law descends to the continuous-path pushforward. The only input is the (J1) stationarity field; no invariance is assumed on the target law.
The transported fresh-shell law is a translation-invariant measure. This is
the analogue of vaddInvariantMeasure_zeroShellRegLaw, and together with the
two measurability instances above it completes the carrier data required by the
Ω-level decorrelation chain.
The transported origin forcing #
The literal matrix-vector forcing at the spatial origin, read on the
continuous-path carrier. This is the same formula as
ShellField.originForcing, with the argument a continuous path instead of an
CoarseGraining regular field.
Equations
Instances For
Matrix-vector multiplication is continuous in the matrix.
The transported L² layer #
The transported forcing is square integrable, from the frozen (J2) Gaussian
tail through ShellField.memLp_originForcing_of_j2_tail.
The canonical fresh-shell Helmholtz splitting at the transported carrier #
The transported origin forcing as an element of the stationary L² layer of
the continuous-path carrier.
Equations
Instances For
The canonical source-sign potential corrector at the transported carrier: the
negative of the orthogonal projection of the forcing onto the stationary
potential subspace, the exact analogue of
ShellField.zeroShellPotentialCorrector on CoarseGraining's carrier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A strongly measurable representative of the canonical corrector.