Closure #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The conditional sensitivity estimate for the response functional #
The source argument is, with M := max_{t ∈ [0,1]} J(a + t h) and
E := |p|² ‖h‖_{W^{1,∞}}² λ⁻¹ + |p·q| ‖∇h‖_{W^{1,∞}}² λ⁻² ,
the coarse-grained derivative bound
l.Dh.boundat the pointa + t h, together with the conditionallambdasensitivity estimate (which keeps the gauge along the segment within a factor two of the base gauge), gives|d/dt J(a + t h)| ≤ C E^{1/2} M^{1/2} + C ‖∇h‖ λ⁻¹ M for all t ∈ [0,1];integration in
tturns this into the self-referential boundM ≤ J(a) + C E^{1/2} M^{1/2} + C ‖∇h‖ λ⁻¹ M;Young's inequality absorbs the two
Mterms on the right, which under the smallness gate‖∇h‖ ≤ C⁻¹ λyields the frozen conclusion.
Step 1 uses the D_h bound Provider.DhBound.coarseMatrixDerivative_bound,
which holds at every coefficient field on the unit cube, hence in particular
at every point of the segment; the derivative itself is the
Provider.Path.responseJ_derivative transported along the path semigroup
(Response.PathDerivative). Step 2 is the mean-value step
Response.le_add_of_hasDerivAt_le applied at the maximum point, which exists
because t ↦ J(a + t h) is differentiable, hence continuous, on the compact
segment. Step 3 is
Provider.Multiscale.DiscreteCompounding.self_bound_le_closed.
The gauge control of step 1 is supplied by
Response.pathGauge_le_two_mul_of_cube_dhFluxForm_bound, whose single analytic
input hcube (the pure-flux D_h bound on all triadic descendants of the unit
cube, with the root gauge as coefficient) is a premise of the provider below.
Arithmetic of the pointwise derivative bound #
The self-referential bound along the segment #
The provider, given the descendant pure-flux D_h bound #
The conditional sensitivity estimate for the response functional, given
the per-descendant pure-flux D_h bound hcube with the root gauge as
coefficient.
The conclusion is exactly the frozen statement
Algsuperdiff.Frozen.Section24.responseJ_sensitivity, with exactly the frozen
binders; the only extra hypothesis is hcube, which is a consumption point
and carries no proof step of the frozen statement: it is the p = 0
specialization of the D_h bound applied on all triadic descendants of the
unit cube, i.e. the hcube input of
Provider.Lambda.Spine.unitCubeLambda_inv_perturb_le_of_cube_dhFluxForm_bound.
The explicit constant is C = 8 K₀ + 4 C₁ + 4 C₁², where C₁ is the constant
of the D_h bound and K₀ the constant of hcube.
The provider #
The conditional sensitivity estimate for the response functional.
This is the provider form of the frozen target
Algsuperdiff.Frozen.Section24.responseJ_sensitivity, with exactly the frozen
binders. The premise hcube of
responseJ_sensitivity_of_cube_dhFluxForm_bound is discharged here by
Provider.Lambda.Closure.abs_dhFluxForm_le_root_gauge, the descendant D_h
bound with the root coarse gauge that also drives the lambda sensitivity
provider.
The explicit constant is C = 8 C₀(d) + 4 C₁(d) + 4 C₁(d)², where C₁(d) is
the constant Provider.DhBound.dhBoundConst d of the D_h bound and C₀(d) = Provider.Lambda.fluxSpineConst d.