JCarrierRescale

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

Transport of the response-J sensitivity to a translated triadic cube

This module is the cube-carrier transport provider used toward the J-carrier rescaling of p.bfA.multiscalebound in ABK26. It proves the exact translation/dilation identity and a conditional bad-event response estimate, but it does not by itself close an unfrozen source node.

The manuscript checks the smallness hypothesis e.J.sensitivity.smallness.condition at the cube z + square_j and then writes "Applying e.J.by.means.of.bfA and then Lemma l.J.sensitivity with delta = 1 yields.". Lemma l.J.sensitivity is stated at the unit cube square_0, and the frozen Section 2.4 realization Algsuperdiff.Frozen.Section24.responseJ_sensitivity is stated at the unit-cube carrier cubeDomain (originCube d 0) as well. This module exposes that transport, as an equality — so the dimension-only constant is untouched — and reads the proved #J-smallness conclusion through it.

The transport

LambdaCovariance.lean already supplies the transport for the multiscale lower ellipticity: unitCubeLambda s q (unitRescaledCutoffCoeff M Q n omega) = lambda_{s,q}(Q; a_n(omega)). What was missing is the same identification for the response functional itself,

J(square_0, p, q; a_n(z + 3^j .))  =  J(z + square_j, p, q; a_n) ,

which is assembled here from two CoarseGraining interfaces:

• Translation. Internal.Ch02.book_responseJ_eq_ResponseJ rewrites the Chapter 2 response as the raw ResponseJ of the coefficient field on the open cube; ResponseJ_translateSet_eq_translateCoeffField is its covariance under a real translation of the domain; and Cutoff.coefficientCutoff_translateCutoffSample moves the translation from the coefficient field to the sample. The geometry is CoarseGraining's openCubeSet_eq_translateSet_originCube_of_triadicCube.
• Dilation. Ch02.responseJ_dilate applied to Ch02.TriadicCoeffFamily.isDilation_dilate, at dilateCube (-m) (originCube d m) = originCube d 0.

Both are exact identities: J is scale free and translation covariant, so no constant is created or lost.

Main results

• responseJ_cutoff_translateCutoffSample: translation covariance of the Chapter 2 response for the actual coefficient cutoff.
• responseJ_originCube_dilate: scale normalization of the response.
• responseJ_unitRescaledCutoffCoeff: the exact transport identity, J(square_0, p, q; a_n rescaled) = J(z + square_j, p, q; a_n).

References

• ABK26 (p.bfA.multiscalebound, the carrier transport).
• ABK26 (l.J.sensitivity, stated at square_0).

Translation covariance of the coarse-grained response

theorem Algsuperdiff.Section3.Provider.Multiscale.responseJ_cutoff_translateCutoffSample {d : ℕ} (M : ABKModel d) (m : ℤ) (v : HCPolySupport.Vec d) {R T : HCPolySupport.TriadicCube d} (hset : HCPolySupport.openCubeSet T = HCPolySupport.translateSet v (HCPolySupport.openCubeSet R)) (p q : HCPolySupport.Vec d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain T) ((Cutoff.coefficientCutoffTriadicCoeffFamily M m omega).coeffOn T) p q = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) ((Cutoff.coefficientCutoffTriadicCoeffFamily M m (Cutoff.translateCutoffSample v omega)).coeffOn R) p q

One-cube translation covariance of the Chapter 2 response for the actual coefficient cutoff: if the open realization of T is the translate by v of that of R, then the response of the cutoff at T equals the one at R for the translated sample.

Scale normalization of the coarse-grained response

theorem Algsuperdiff.Section3.Provider.Multiscale.responseJ_originCube_dilate {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) ((HCPolySupport.Book.Ch02.TriadicCoeffFamily.dilate (-m) F).coeffOn (HCPolySupport.originCube d 0)) p q = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m)) (F.coeffOn (HCPolySupport.originCube d m)) p q

Scale normalization of the Chapter 2 response. The response of a family on the centered scale-m cube is that of its 3^{-m}-dilation on the unit cube.

The transport

theorem Algsuperdiff.Section3.Provider.Multiscale.responseJ_unitRescaledCutoffCoeff {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (p q : HCPolySupport.Vec d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (BadEvents.unitRescaledCutoffCoeff M Q cutoffScale omega) p q = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) ((Cutoff.coefficientCutoffTriadicCoeffFamily M cutoffScale omega).coeffOn Q) p q

The response-J carrier transport (the J-carrier rescaling of p.bfA.multiscalebound, ABK26). The frozen unit-cube response functional of the rescaled coefficient object is the response functional of the cutoff on the translated triadic cube Q = z + square_j itself:

J(square_0, p, q; a_n(z + 3^j .))  =  J(z + square_j, p, q; a_n) .

This is the exact analogue, for J, of the proved unitCubeLambda_unitRescaledCutoffCoeff.

The conditional response estimate at the translated triadic cube