UglyPre #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 2 of p.mathcalE.annular.decomp: the sensitivity estimate at the #
(mu, sigma_0, h)-witness
ABK26, Section 4.1, (e.ugly.estimate.for.J.pre). The manuscript
localizes the response functional by applying the unconditional
sensitivity estimate l.J.sensitivity.no.conditions at the witness
mu := sigmaBar_m * sigmaBar_{n-2}^{-1} ,
sigma_0 := sigmaBar_{n-2} ,
h := k_L - (k_L - k_m)_{cube_m} - k_{n-2}
on each cube z + cube_n. This module proves that instantiation over the
proved running diffusivity, from the Section 2.4 anchor
Algsuperdiff.Frozen.Section24.responseJ_sensitivity_unconditional.
The witness is exactly what makes the display's left side the manuscript's
J(., sigmaBar_m^{-1/2} e, sigmaBar_m^{1/2} e): the anchor's load pair is at
the product gauge mu * sigma_0, and here mu * sigma_0 = sigmaBar_m. That
identity is the arithmetic content of the parameter choice, and it is proved,
not assumed.
Two forms #
exists_responseJ_ugly_pre_terms-- the anchor's terms at the witness. This is the shape the downstream per-term collapse consumes (each of the anchor's last two terms is patched separately).exists_responseJ_ugly_pre-- the manuscript's printed three-term display, obtained from the four-term form by packaging the anchor's third and fourth terms into the single last termC ((sigmaBar_m^{-1} + lambda^{-1}) ||grad h||)^2.
The s <= 1/4 range #
The cited lemma requires BOTH of its exponent slots in (0, 1/4]. The
t-slot is the enclosing proposition's s, which ranges over
[8 gamma, 1/2]. The interval s in (1/4, 1/2] is therefore NOT covered by
the citation. Both theorems here carry the honest hypothesis s <= 1/4 (and
the implied gamma <= 1/8); the uncovered range is an acknowledged gap, not
something narrowed silently.
Two silent normalizations, not discharged here #
The manuscript's display sits on the translated, rescaled cube z + cube_n
while the cited lemma is stated on the unit cube cube_0, and it replaces the
lemma's ||grad h||_{W^{1,infinity}(cube_0)} by the scale-normalized
3^{2n} ||grad(k_L - k_{n-2})||_{W-underline^{1,infinity}(z+cube_n)}. Neither
change of variables is performed in the source. Here the coefficient a, the
skew perturbation h and hence the gauge h.gradientW1Infinity are the
caller's data on the unit cube, so both normalizations remain exactly where the
manuscript leaves them: at the instantiation site.
Two carrier bridges #
The frozen W^{1,infinity} gauge of a skew perturbation is nonnegative: it is
a maximum of two ENNReal.toReal values.
Step 2 at the witness: the four anchor terms #
e.ugly.estimate.for.J.pre, four-term form.
The unconditional sensitivity estimate at mu = sigmaBar_m sigmaBar_{n-2}^{-1}, sigma_0 = sigmaBar_{n-2}, with the lemma's s-slot at
gamma and its t-slot at the caller's s. The load pair on the left is the
manuscript's, because mu * sigma_0 = sigmaBar_m.
The four summands are, in order, the anchor's T_1--T_4. The manuscript
packages T_3 and T_4; see exists_responseJ_ugly_pre.
The printed three-term display #
e.ugly.estimate.for.J.pre, as printed.
The manuscript's three-term display: the two sensitivity terms with their
(1 + ||grad h|| lambda^{-1}) growth factors, and the single packaged
gradient term C ((sigmaBar_m^{-1} + lambda_{gamma,2}^{-1}) ||grad h||)^2.