ResponseSubadditivity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Response subadditivity patching for the homogenization-error bridge #
The proof of the unconditional sensitivity estimate
(l.J.sensitivity.no.conditions of ABK26) opens with the display
J(cu_0, P, Q; a) <= avsum_{z in 3^{-h} Zd cap cu_0} J(z + cu_{-h}, P, Q; a),
that is, the root response at a fixed loading is dominated by the unweighted
average of the descendant responses at the same loading. This module records
that step as a named node, together with the monotonicity in the depth h
which it implies. Both are stated in the CoarseGraining triadic-family
vocabulary: descendantsAverage Q j is exactly avsum_{z in 3^{scale(Q) - j} Zd cap Q}.
The two structural inputs are CoarseGraining's responseJ_subadditive (the
CoeffOn-level subadditivity over an arbitrary DomainPartition) applied to
descendantsDomainPartition Q j, and the identification of the corresponding
weightedAverage with descendantsAverage. No representative, ellipticity or
admissibility premise is required: TriadicCoeffFamily already carries the
restriction compatibility on nested open cubes.
Response subadditivity patching. For a triadic coefficient family and
a depth j, the response on a cube is bounded by the unweighted average of the
responses of the depth-j descendants at the same loading (p, q).
This is the opening display of the proof of l.J.sensitivity.no.conditions in
family vocabulary.
The descendant averages of the response at a fixed loading are nondecreasing
in the depth. This is the iterated form of
responseJOnCube_le_descendantsAverage_responseJ, obtained from the tower
property of descendantsAverage.