ResponseTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The response transport: J(z+□_n; ã_{L,m}) at the unit-cube perturbation #
ABK26, Section 4.1, Step 2 of p.mathcalE.annular.decomp writes
we apply Lemma
l.J.sensitivity.no.conditionswithμ := σ_m σ_{n−2}^{-1},σ₀ := σ_{n−2}andh := k_L − (k_L − k_m)_{□_m} − k_{n−2}to each cubez + □_n
and obtains a bound whose left-hand side is J(z+□_n, σ_m^{-1/2}e, σ_m^{1/2}e; ã_{L,m}) with ã_{L,m} = a_L − (k_L − k_m)_{□_m}. The cited
lemma is stated on the unit cube □₀ only, so the single word "apply"
compresses a translation and a dilation. (Its error half is
ErrorTransport.lean; the λ half was already proved as
unitCubeLambda_unitRescaledCutoffCoeff.)
The identity #
For every triadic cube Q = z + □_j, every L above the cutoff level, and
every antisymmetric constant C,
J(Q, p, q; a_L − C)
= J(□₀, p, q; a_{lowScale}(z + 3^j ·) + 1 · (h − C)) ,
where the perturbation on the right is the frozen W^{2,∞} carrier
Provider.Diffusivity.ApproximateRecurrence.centeredShellUnitCube, i.e. the
manuscript's centered fresh shell rescaled onto the unit cube. Both sides are
the same number; no constant and no inequality direction is introduced.
Route #
Three proved steps and one new one.
- Translation (new here).
Internal.Ch02.book_responseJ_eq_ResponseJis stated at a fully general(U : Domain d)and(a : CoeffOn U), so it rewrites the Chapter 2 response of theã_{L,m}object as the rawResponseJof its representative;ResponseJ_translateSet_eq_translateCoeffFieldis the covariance under a real translation of the domain; andCutoff.coefficientCutoff_translateCutoffSamplemoves the translation from the field to the sample. The subtracted constant is translation-inert, so the route is exactly that of the provedProvider.Multiscale.responseJ_cutoff_translateCutoffSample. - Dilation (proved, family-general).
Provider.Multiscale.responseJ_originCube_dilateis stated for an arbitraryTriadicCoeffFamily, so it applies tosubConstCutoffTriadicCoeffFamilywith no change. - The shell link (new here).
CoeffOn.dilatestores an internalpointwiseCoeffFieldrepresentative, not the literal rescaled field, so the dilatedã_{L,m}object and the perturbed object are compared through their a.e. descriptions:unitRescaledSubConstCoeff_toCoeffField_ae_eqsays the first is a.e. the rescaled cutoff field minusC, andApproximateRecurrence.centeredShellUnitCube_shiftsays the second is pointwise exactly that.Ch02.responseJ_eq_ofAEEqcloses the comparison.
The a.e. description is obtained by running the two dilation identities — the
one for subConstCutoffTriadicCoeffFamily and the one for
Cutoff.coefficientCutoffTriadicCoeffFamily — against each other: the
representative-level pullback dilateCoeffField is a precomposition, so
subtracting a constant commutes with it definitionally.
Almost-everywhere, and why #
Unlike the error transport of ErrorTransport.lean, this identity is proved
through a genuine a.e. comparison of two coefficient objects. No null set
survives into the conclusion.
References #
- ABK26, (
ã_{L,m}), (e.ugly.estimate.for.J.pre), (e.ugly.estimate.for.J), (l.J.sensitivity.no.conditions, stated on□₀).
Translation covariance at the constant-shifted cutoff #
One-cube translation covariance of the Chapter 2 response for
ã_{L,m} = a_L − C. If the open realization of T is the translate by v
of that of R, then the response of a_L − C at T equals the one at R for
the translated sample. The subtracted constant is translation-inert, so it
simply rides along.
This is the exact analogue, at the constant-shifted field, of the proved
Provider.Multiscale.responseJ_cutoff_translateCutoffSample.
The rescaled unit-cube object of ã_{L,m} #
The constant-shifted cutoff a_L − C, rescaled from the cube Q = z + □_j to
the unit cube by the manuscript's map y ↦ z + 3^j y, as a unit-cube
coefficient object. This is the ã_{L,m} sibling of the proved
Provider.BadEvents.unitRescaledCutoffCoeff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The response transport, unrescaled form. The response of the rescaled
ã_{L,m} object on the unit cube is the response of ã_{L,m} on the cube Q
itself.
The a.e. description of the rescaled field #
The coefficient field of the rescaled ã_{L,m} object is, almost everywhere
on the open unit cube, the rescaled cutoff field minus the constant.
The proof runs the two dilation identities against each other: the
representative-level pullback dilateCoeffField is a precomposition, so
subtracting a constant commutes with it definitionally. No literal description
of either side is needed.
The shell link #
The dilated ã_{L,m} object is the frozen perturbed object. The
rescaled a_L − C coefficient object and the frozen perturbCoeffOn of the
rescaled a_{lowScale} by the manuscript's centered fresh shell at t = 1
agree almost everywhere on the open unit cube.
ApproximateRecurrence.centeredShellUnitCube_shift supplies the pointwise
identity for the right-hand side; the only a.e. step is the internal
representative that CoeffOn.dilate selects on the left.
The transport #
The response transport of ã_{L,m} (the response half of ABK26's silent
rescaling).
The Chapter 2 response of the manuscript's ã_{L,m} = a_L − C on an arbitrary
triadic cube Q = z + □_j is exactly the unit-cube response of the frozen
perturbed object that the Section 2.4 sensitivity anchor consumes: the rescaled
cutoff a_{lowScale}(z + 3^j ·) perturbed at t = 1 by the manuscript's
centered fresh shell.
This is the identification the manuscript performs silently when it applies the
unit-cube lemma l.J.sensitivity.no.conditions "to each cube z + □_n". It is
an equality, so no constant is created and no inequality direction is fixed.
The response transport at the Section 4 lattice enumerations. The same
identity at the cube ⟨n, v⟩ = 3^n v + □_n and at the 𝒢₂ cutoff level
n − 2, i.e. in the exact spelling in which the ugly chain reads it.
The manuscript's own constant #
The manuscript's averaged flux increment (k_L − k_m)_{□_m} is
antisymmetric as a matrix, in the matTranspose spelling the constructions
above require. This is the entrywise Support.fluxIncrementAverage_skew.
The response transport at the manuscript's own ã_{L,m}. The constant is
(k_L − k_m)_{□_m}, whose antisymmetry is the proved
Support.fluxIncrementAverage_skew, and the cube is the lattice cube ⟨n, v⟩.
This is the left-hand side of e.ugly.estimate.for.J.pre read at the unit-cube
object that the frozen sensitivity anchor consumes.