ResponseCongruence

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

The perturbed rescaled coefficient is the rescaled a_L, for responseJ

LambdaTransfer.lean proves perturbCoeffOn_unitRescaledCutoffCoeff_toCoeffField_ae_eq: the coefficient of the frozen perturbation

perturbCoeffOn (unit cube) (a_n rescaled) (k_L - k_n rescaled) 1

agrees, almost everywhere on the open unit cube, with the rescaling `y |-> a_L(z

• 3^m y)of the literal cutoffa_L(ABK26). LambdaCovariance.leanproves the same description for the honest rescaled objectunitRescaledCutoffCoeff M Q L omega`.

The consumer of the #J-smallness step needs the two objects to be interchangeable inside responseJ. Nothing analytic is reproved here; this module records the identification of the two CoeffOn objects and reads the congruence at it.

Main results

• perturbCoeffOn_unitRescaledCutoffCoeff_aeEq: the two unit-cube coefficient objects are CoeffOn.AEEq.
• responseJ_perturbCoeffOn_unitRescaledCutoffCoeff: the responseJ congruence, J(square_0, p, q; a_n + (k_L - k_n) rescaled) = J(square_0, p, q; a_L rescaled).
• unitCubeLambda_perturbCoeffOn_unitRescaledCutoffCoeff: the same identification read at the frozen unit-cube gauge, which is the form the lambda-sensitivity consumer needs.

References

• ABK26 (p.bfA.multiscalebound, the #J-smallness consumer).
• ABK26, e.good.local.events.

The two unit-cube coefficient objects agree almost everywhere

theorem Algsuperdiff.Section3.Provider.BadEvents.perturbCoeffOn_unitRescaledCutoffCoeff_aeEq {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {n L : ℤ} (hnL : n ≤ L) (omega : Cutoff.CutoffSample d) : (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (unitRescaledCutoffCoeff M Q n omega) (incrementUnitCube₂ Q n L omega).toLInfSkewMatrixFieldOn 1).AEEq (unitRescaledCutoffCoeff M Q L omega)

The #J-smallness identification, as a CoeffOn a.e. equality (ABK26). The frozen perturbation of the rescaled a_n by the rescaled literal increment k_L - k_n is a.e. equal, on the open unit cube, to the rescaled a_L.

The responseJ congruence

theorem Algsuperdiff.Section3.Provider.BadEvents.responseJ_perturbCoeffOn_unitRescaledCutoffCoeff {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {n L : ℤ} (hnL : n ≤ L) (omega : Cutoff.CutoffSample d) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (unitRescaledCutoffCoeff M Q n omega) (incrementUnitCube₂ Q n L omega).toLInfSkewMatrixFieldOn 1) p q = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (unitRescaledCutoffCoeff M Q L omega) p q

The responseJ congruence of the #J-smallness consumer (ABK26). The frozen response functional of the perturbed rescaled a_n is the response functional of the honest rescaled a_L.

theorem Algsuperdiff.Section3.Provider.BadEvents.unitCubeLambda_perturbCoeffOn_unitRescaledCutoffCoeff {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {n L : ℤ} (hnL : n ≤ L) (omega : Cutoff.CutoffSample d) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : Frozen.Section24.unitCubeLambda s q (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (unitRescaledCutoffCoeff M Q n omega) (incrementUnitCube₂ Q n L omega).toLInfSkewMatrixFieldOn 1) = Frozen.Section24.unitCubeLambda s q (unitRescaledCutoffCoeff M Q L omega)

The same identification at the frozen unit-cube multiscale gauge: the lambda-sensitivity consumer of ABK26 reads its conclusion at lambda_{s,q} of the perturbed object, which is lambda_{s,q} of the rescaled a_L.