PrincipalResponseLegsIndep #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: sub-step (iii) of the principal response, the independence step #
Source display in ABK26:
e.lower.bound.principal.one.pre(label; display), whose derivation is the sentence:Therefore, by independence of bfA_{m-h} and G_{-(h)_{z+cu_n}} P_z (the latter is a function of k_m - k_{m-h}), ...
The content of that sentence, and the only content of this module, is that the expectation of the doubled quadratic form
G_{-(h)_{z+cu_n}} P_z . bfA_{m-h}(z+cu_n) G_{-(h)_{z+cu_n}} P_z
may be computed by replacing the random matrix bfA_{m-h}(z+cu_n) by its
entrywise expectation, the manuscript's bfAhom_{m-h}(z+cu_n), while the load
is held fixed. In the source's index conventions the matrix is a function of
the shells at or below m - h and the load is a function of the fresh shell
k_m - k_{m-h}, i.e. of the shells in (m-h, m]; these two index blocks are
disjoint, so the cross-shell independence of ABK26 applies.
There is no Jensen step and no convexity step here, and none is used below: the load is not averaged, only the matrix is.
The two carrier binders, and why neither is a proof step #
integral_blockQuadratic_shellSplit_eq carries exactly two measurability
binders, and both are the manuscript's own descriptions of its objects rather
than steps of its argument:
hWmeas, that the load is measurable for the fresh block(n, m]. This is the parenthetical "the latter is a function ofk_m - k_{m-h}" and nothing more; the fresh shell it names is the repository'sCutoff.finiteShellIncrement.hBmeas, that the matrix is measurable for the null completion of the lower-shell local field at indexL <= n. This is the statement thatbfA_{m-h}is built from the shells at or belowm - h; the completion, not the bare lower field, is used because the genuine infinite lower cutoff is only measurable after completion (Cutoff.lowerShellLocalCompletion).
The independence itself is not a binder: it is obtained from
Cutoff.indep_lowerShellLocalCompletion_shellIndexSigma_Ioc, hence from
ShellLawPrefix.independent alone.
The integrability binders hB, hW are the manuscript's own standing moment
information: hW is the second-moment content of e.nablaw.in.L.eight
(label), quoted in the display immediately above, and hB is entrywise
integrability of the coarse matrix, which is what makes bfAhom_{m-h}(z+cu_n)
a matrix at all.
Main results #
integral_blockQuadratic_eq_of_indepFun-- the factorization at the level of the2ddoubled coordinates, from pairwise independence.integral_blockQuadratic_eq_of_indep-- the same from independence of two sub-sigma-fields.integral_blockQuadratic_shellSplit_eq-- the shell-block form: past shells against a fresh range.
The doubled quadratic form over the 2d doubled coordinates #
The factorization #
The independence factorization, at the doubled coordinates. If every
entry of the random doubled matrix B is independent of every product of two
coordinates of the random doubled load W, then the expected quadratic form is
unchanged when B is replaced by its entrywise expectation Bbar.
The load is held fixed throughout; only the matrix is averaged.
The independence factorization, at two sub-sigma-fields. The same factorization when the matrix is measurable for one sub-sigma-field, the load for another, and the two are independent.
The shell-block form #
The independence factorization at the shell blocks. A doubled matrix
measurable for the completed lower-shell field at index L, against a doubled
load measurable for a fresh shell range (n, m] lying above L: the expected
quadratic form is computed at the entrywise expectation of the matrix.
The independence is not assumed: it is
Cutoff.indep_lowerShellLocalCompletion_shellIndexSigma_Ioc, i.e. ABK26 in
block form.