BlockResponse #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.bfJ.general: the block response at the isotropic comparator, in scalar J #
ABK26, (the itemized property e.bfJ.general) and its use in the first
display of the proof of p.mathcalE.annular.decomp (with the transpose
remark):
bfJ(U, (p,q), (q*,p*); a) = 1/2 J(U, p-p*, q*-q; a) + 1/2 J(U, p*+p, q*+q; a^t) .
The identity itself is proved upstream and unconditional: it is
CoarseGraining's Book.Ch02.doubledResponseJ_eq_half_responseJ_adjoint_sum,
the public accessor of the doubled-response theory available for every CoeffOn U. What this module supplies is the conversion the manuscript actually
performs with it: the normalized block-response maximum over the
2d-dimensional full-block unit sphere, which is the inner quantity of
d.mathcal.E, is bounded by the sum of the scalar maxima at the loads
(sigma0^{-1/2} e, sigma0^{1/2} e) for the field and for its transpose.
The mechanism, and why the constant is 1 #
For a0 = sigma0 I one has bfA_0 = diag(sigma0 I, sigma0^{-1} I), so a member
of the normalized value set is bfJ(U, P, bfA_0 P) with the representation-free
normalization <P, bfA_0 P> = 1, i.e. sigma0 |p|^2 + sigma0^{-1} |q|^2 = 1
for P = (p, q). The splitting identity evaluates it at
u := p - sigma0^{-1} q , v := p + sigma0^{-1} q ,
bfJ = 1/2 J(a, u, sigma0 u) + 1/2 J(a^t, v, sigma0 v) ,
and both scalar loads are of the manuscript's shape
(sigma0^{-1/2} f, sigma0^{1/2} f) with f = sigma0^{1/2} u resp.
g = sigma0^{1/2} v. Quadratic homogeneity of J in the load pair turns them
into |f|^2 resp. |g|^2 times the value at a unit direction, and the
normalization gives exactly
sigma0 |u|^2 + sigma0 |v|^2 = 2 (sigma0 |p|^2 + sigma0^{-1} |q|^2) = 2 ,
so each half-weight is at most 1: the conversion holds with constant 1, well
inside the manuscript's C.
What is proved #
responseJ_scalarLoad_le_of_unit_bound-- the homogeneity step.normalizedBlockResponseMax_scalarMatrix_le-- the one-cube conversion.maxDescendantNormalizedBlockResponseAtScale_scalarMatrix_le-- the same over a whole descendant family, which is the shape the(infinity,2)scale sum reads.responseJ_transpose_scalarLoading_le_normalizedBlockResponseMax-- the reverse inequality for the transposed field, the mirror of the proved Section 2.4 bound for the field itself; in particular the transposed scalar value set is bounded above, so a caller may form its supremum...._isotropicComparator_le-- the conversions in the Section 3/4 spelling (Observable.isotropicComparatorMatrix,Observable.inverseSqrtLoad,Observable.sqrtLoad), i.e. literally the manuscript'sJ(., sigmaBar^{-1/2} e, sigmaBar^{1/2} e).
The homogeneity step #
Quadratic homogeneity at the scalar loading. If the response at every
unit load pair (sigma0^{-1/2} e, sigma0^{1/2} e) is at most B, then at the
general pair (u, sigma0 u) -- which is that shape at the vector
sigma0^{1/2} u -- it is at most sigma0 |u|^2 B.
The block-load structure at an isotropic background #
The two structural facts about a normalized block probe: its co-load is the
image under the constant block matrix, and its quadratic normalization is 1.
Both are representation free -- the matrix square root never has to be
computed.
The conversion #
e.bfJ.general, in the form the manuscript uses it.
At the isotropic background sigma0 I, the normalized block-response maximum of
one cube -- the maximum of the doubled response over the 2d-dimensional unit
sphere, i.e. the inner quantity of d.mathcal.E -- is bounded by the sum of two
scalar bounds: one for the field a and one for its transpose a^t, each taken
over the scalar loads (sigma0^{-1/2} e, sigma0^{1/2} e) with |e| = 1.
The constant is 1; the manuscript's display carries a C(d).
The conversion over a whole descendant family. This is the shape the
(infinity,2) scale sum of mathcal E_{s,infinity,2} reads at one scale.
The mirror bound for the transposed field #
The a-side of the reverse inequality is proved in the Section 2.4 bridge
(responseJ_scalarLoading_le_normalizedBlockResponseMax), whose doubled probe
is (e/sqrt 2, -e/sqrt 2) in the normalized coordinates. Flipping that sign
selects the adjoint summand of the same splitting identity, which gives the
transpose analogue below. Together with the conversion above, the block
maximum and the two scalar maxima control each other, so the transposed scalar
value set is bounded above -- which is what lets a caller form its supremum at
all.
The normalized block probe used for the transposed annular response.
Equations
Instances For
The mirror of the Section 2.4 scalar-loading bound, for the transposed field. The transposed scalar response at the normalized loading is one of the normalized block-response values, hence at most the block maximum. In particular the transposed value set is bounded above.
The Section 3/4 spelling #
The one-cube conversion at the Section 3 comparator literal
sigma Id, with the loads written as the Section 3 observables
sigma^{-1/2} e and sigma^{1/2} e.
The descendant-family conversion at the Section 3 comparator literal.