Step3HSlot #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 3: the sensitivity estimate at the recentered h-slot, at scale j #
The target #
Step 3 of the proof of l.bounds.mathcal.E.aL applies
the sensitivity estimate
e.J.sensitivity.no.conditionsof Lemmal.J.sensitivity.no.conditionsin the cube□_jwithμ := σ_m σ_{j-2}^{-1},σ₀ := σ_{j-2}andh := k_L − k_{j-2} − (k_L − k_m)_{□_m}
to the single J-moment produced by Steps 1--2, "as in e.ugly.estimate.for.J.pre
in Step 2 of the proof of Proposition p.mathcalE.annular.decomp".
That template is already proved in this repository, for §4.1, at the SAME
witness family and with the SAME recentered h-slot:
Annular.exists_responseJ_ugly_pre(Provider/Annular/UglyPre.lean) — the Section 2.4 anchorFrozen.Section24.responseJ_sensitivity_unconditionalinstantiated atμ = σ_m σ_{n-2}^{-1},σ₀ = σ_{n-2}, with the caller's unit-cube coefficientaand unit-cube skew perturbationh, and with the anchor'st-slot at the caller'ss;Annular.responseJ_fluxCorrectedConst_lattice_eq_perturbCoeffOn(Provider/Annular/ResponseTransport.lean) — the translation/dilation identity that readsJ(z + □_n; a_L − (k_L − k_m)_{□_m})as the unit-cube perturbed object the anchor consumes, with the recentering constant folded into the unit-cube perturbationcenteredShellUnitCube.
What the export gives, and why that shape #
The conclusion bounds
J(3^j v + □_j , σ_m^{-1/2} e , σ_m^{1/2} e; a_L − (k_L − k_m)_{□_m})
by a right-hand side not containing e. That is exactly the hypothesis
shape hfld of the proved primal/adjoint split
Annular.normalizedBlockResponseMax_isotropicComparator_le (e.bfJ.general,
constant 1), which is the step that connects this display to the block
response maximum appearing in d.mathcal.E — i.e. to the inner object of the
Step-1 endpoint of Step1ScaleSum.lean.
Deviations from the printed display, all inherited #
- The gapped gauge. The printed exponents of
e.apply.sensitivity.J.aLare2s/(1-2γ)and2γ/(1-2γ); the display below carries2s/(1-4γ)and4γ/(1-4γ), and itsλ-slots readunitCubeLambda (2γ). A warning about direction: antitonicity ofλ⁻¹in the gauge means the conclusion can never be read back at gaugeγ. - The unit-cube gauges. The right side is written in the anchor's
unit-cube gauges (
h.gradientW1Infinity,h.valueL2,unitCubeLambda,unitCubeHomogenizationError), not in the printed scale-normalized ones (3^{2j} ‖∇(k_L − k_{j-2})‖_{W^{1,∞}(□_j)},‖·‖_{L²(□_j)},λ_{γ,2}^{-1}(□_j; a_{j-2}),𝓔_{s,2,2}(□_j; a_{j-2}, σ_{j-2})). The manuscript performs that replacement silently; §4.1 records it as a named divergence and leaves it at the instantiation site, and so does this module. Supplying the identification is Step 4's business (its bullets (B4)--(B6) are stated in exactly those normalized gauges). s ≤ 1/4. The cited lemma needs both exponent slots in(0, 1/4]. This is free at §4.5, whose owns-range is[C² √γ, 1/4]with the closed right endpoint;γ ≤ 1/8is likewise free fromγ ≤ C^{-10}.
Main result #
exists_responseJ_step3_recentered— the Step-3 field-leg display at the lattice cube3^j v + □_j, for everyjwithj - 2 ≤ L, every recentering indexm, and every unite, with ane-free right-hand side.
References #
- ABK26,
l.bounds.mathcal.E.aL, (Step 3 ande.apply.sensitivity.J.aL);l.J.sensitivity.no.conditions;e.ugly.estimate.for.J.pre;e.bfJ.general.
Step 3, field leg. The Section 2.4 sensitivity anchor, instantiated at §4.5's own witness
μ := σ_m σ_{j-2}^{-1} , σ₀ := σ_{j-2} , h := k_L − k_{j-2} − (k_L − k_m)_{□_m} ,
read at the lattice cube 3^j v + □_j through the proved response transport.
The right-hand side does not mention e, so it is directly usable as the
primal half of Annular.normalizedBlockResponseMax_isotropicComparator_le.
The three summands are the printed ones of e.apply.sensitivity.J.aL, in the
anchor's unit-cube gauges and at the gapped gauge s = 2γ; see the
module docstring for the complete deviation list.