CombineIntegerDownscale #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 2 of p.combine.under.S: the squared means-downscale-by-defect estimate #
ABK26, Step 2 of Proposition p.combine.under.S. The step opens by taking the
expectation of the coarse-grained identity e.J.coarse.grained and combining
it with subadditivity e.subaddJ.nosymm and the vanishing annealed coupling
e.annealed.khom.zero to get, for scale indices n <= m and e, e' with |e| = 1,
0 <= shom_{L,*}^{-1}(cu_n) - shom_{L,*}^{-1}(cu_m)
= 2 E[ J(cu_n, 0, e; a_L) - J(cu_m, 0, e; a_L) ]
<= 2 E[ J(cu_n, e', e; a_L) - J(cu_m, e', e; a_L) ]
and then, under the load normalization e.pq.normed, the printed display
0 <= shom_{L,*}^{-1}(cu_n) - shom_{L,*}^{-1}(cu_m)
<= 2 shom_{L,*}^{-1}(cu_m) E[ J(cu_n, p, q; a_L) - J(cu_m, p, q; a_L) ] .
The last declaration below states the strictly stronger form obtained by
replacing the right-hand gauge shom_{L,*}^{-1}(cu_m) by
|q|^{-2} = shom_L^{-1}; see Route.
Scope #
The first group of declarations corresponds to the two mean-propagation displays; these carry no constant and no premise beyond the load normalization.
The second group completes Step 2 with the squared estimate
e.means.downscale.by.defect (closed). It consumes the proposition's own
one-cube fourth-moment premise e.moment.bound.onmathcalE and the load
normalization e.pq.normed as hypotheses, in three steps:
- nonnegativity of
E[J(cu_m,p,q;a_L)]and the subadditivity chainE[J(cu_n,p,q;a_L)] <= E[J(cu_L,p,q;a_L)]forL <= n; - the one-cube bound
E[J(cu_L,p,q;a_L)] <= delta_1, obtained from the first inequality ofe.mathcalE.monotone.ordered(in the form of the proved simultaneous directional dominationJ <= E_{s,infinity,2}^2) and Cauchy--SchwarzE[X^2] <= E[X^4]^{1/2}. The sub-cube discounte.bound.one.cube.by.mathcalEis not used: the observed cube and the coefficient cutoff cube are bothcu_L, so itsk = minstance is the identity; - squaring against the
|q|^{-2} = shom_L^{-1}gauge of the first group.
Because the gauge of step 3 is already shom_L^{-1}, the printed step
shom_{L,*}^{-1}(cu_m) <= 2 shom_L^{-1} -- the only place where the moment
premise is used a second time -- is not needed, and the universal constant of
e.means.downscale.by.defect is delivered as the explicit numeral 4.
Rendering of the moment premise #
The printed premise E[E_{s,infinity,2}(cu_L; a_L, shom_L)^4]^{1/2} <= delta_1
asserts in particular that the fourth moment of a nonnegative observable is
finite. Bochner's ∫ returns 0 on a non-integrable function, so the
literal transcription Real.sqrt (∫ ...) <= delta_1 would be satisfied
vacuously by an infinite moment. The premise is therefore carried in its
lower-integral form ∫⁻.ofReal (E^4) <=.ofReal (delta_1 ^ 2), which is exactly
E[E^4] <= delta_1^2 for the nonnegative observable and encodes finiteness and
the bound in one clause. lintegral_ofReal_le_ofReal_sq_of_sqrt_integral_le
converts the Bochner pair (integrability together with the literal Real.sqrt
bound) into it.
The observable itself is Observable.cutoffHomogenizationErrorRepresentative M L L hs (Annealed.sigmaBar M L), the proved measurable representative of
E_{s,infinity,2}(cu_L; a_L, shom_L): coefficient-cutoff scale L, observed
cube cu_L, comparator the genuine running diffusivity shom_L. It is a.e.
equal to the literal CoarseGraining expression by
Observable.cutoffHomogenizationErrorRaw_ae_eq_representative, so the premise
is the same statement as the printed one.
The load normalization is carried as its two printed clauses
q = shom_L p and |q|^2 = shom_L; the derivation uses both (the first to
identify p, the second to identify |q|^2 and the unit direction).
Route #
The printed derivation of the normalized display uses the coefficient-field
homogeneity e.homogeneous.J to move the load (p, q) onto the unit pair
(e', e). That rescaling is not available on the CoeffOn/Domain carriers
of this repository. It is not needed: the annealed coarse-grained identity is
an exact quadratic form in (p, q), so the load enters only through |q|^2 = vecNormSq q and through a second quadratic form in p which is nonnegative by
the same subadditivity input. The conclusion below is therefore obtained with
the load kept general, and it is strictly stronger than the printed display:
the printed right-hand side carries the factor shom_{L,*}^{-1}(cu_m), and
|q|^{-2} = shom_L^{-1} <= shom_{L,*}^{-1}(cu_m) by the unconditional Loewner
monotonicity and infinite-volume limit of e.homs.defs, not by the moment
premise; the moment premise supplies only the opposite half
shom_{L,*}^{-1}(cu_m) <= 2 shom_L^{-1}. The printed display is recoverable
in this repository from
Provider.Diffusivity.ApproximateRecurrence.inv_sigmaBar_le_annealedCubeLowerRight
together with
Provider.Annealed.coefficientCutoffLaw_exists_annealedBlockMatrixAtScale_eq_blockDiag_smul_one.
The e.homogeneous.J bypass now covers the squaring step as well, and there
too no rescaling is performed. The printed proof invokes homogeneity to put
the load in the normalized form the one-cube input expects; but shom_L is a
positive scalar, so e.pq.normed already presents the load in that form:
exists_unit_loads_of_pq_normed certifies that q = shom_L p together with
|q|^2 = shom_L forces (p, q) = (shom_L^{-1/2} e, shom_L^{1/2} e) for the
unit vector e = shom_L^{-1/2} q. The identification is an equality of loads,
not a rescaling of the coefficient field, so the whole file is free of
e.homogeneous.J.
Inputs #
e.J.coarse.grained: CoarseGraining'sintegral_restrictionResponseJObservableCubeSet_eq_quadratic_annealedBlockMatrix, whose integrability side condition is discharged here (not assumed) fromProvider.Annealed.coefficientCutoffLaw_integrable_coarseFullBlockMatrixAtCube.e.annealed.khom.zero:Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrix_lowerLeft_eq_zero.e.subaddJ.nosymm, at every integer scale:Provider.Annealed.coefficientCutoffLaw_matLoewnerLE_annealedSigmaStarInvAtScaleand..._matLoewnerLE_annealedBAtScale.- Scalarity of the annealed inverse-star block on origin cubes:
Provider.Annealed.coefficientCutoffLaw_isScalarMatrix_annealedSigmaStarInvAtScale. - the first inequality of
e.mathcalE.monotone.orderedat the cutoff cube, in the simultaneous directional formProvider.Homogenization.ae_forall_cutoffResponseJ_le_observationHomogenizationError_sq, read atcubeScale = coefficientScale = L, together withObservable.ae_forall_cutoffResponseJ_eq_literal, which identifies the measurable response with the literalJ(cu_L, shom_L^{-1/2} e, shom_L^{1/2} e; a_L).
Main results #
annealedSigmaStarInvScalarAtScalecoefficientCutoffLaw_annealedSigmaStarInvAtScale_eq_smul_onecoefficientCutoffLaw_vecDot_matVecMul_annealedSigmaStarInvAtScalecoefficientCutoffLaw_annealedResponseJAtScale_eq_annealedDiagonalBlockscoefficientCutoffLaw_annealedResponseJAtScale_eq_scalarcoefficientCutoffLaw_annealedResponseJAtScale_sub_eqcoefficientCutoffLaw_annealedSigmaStarInvScalarAtScale_antitone
annealedInverseScalar_scaledDefect_le_responseDefect
*
annealedInverseScalar_defect_le_responseDefect
The scalar shom_{L,*}^{-1}(cu_n) of ABK26 Step 2: the annealed
inverse-star block of the genuine coefficient cutoff on the origin cube at
integer scale n is a scalar matrix, and this is its scalar.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The annealed inverse-star block of the genuine cutoff on an origin cube is
the scalar multiple of the identity determined by
annealedSigmaStarInvScalarAtScale.
Scalar form of the annealed inverse-star quadratic form.
ABK26 e.J.coarse.grained in the mean, with e.annealed.khom.zero.
The expected response of the genuine coefficient cutoff on the origin cube at
any integer scale n is the block-diagonal quadratic form
E[J(cu_n, p, q; a_L)] = 1/2 q. shom_{L,*}^{-1}(cu_n) q - p. q + 1/2 p. bhom_L(cu_n) p.
The mixed block is absent because the annealed coupling of the cutoff law vanishes; the integrability side condition of the expectation identity is discharged from the proved cutoff moment layer, not assumed.
Scalarized form of
coefficientCutoffLaw_annealedResponseJAtScale_eq_annealedDiagonalBlocks.
Exact mean response defect. The p . q terms cancel, so the response
defect between two integer cube scales splits into the inverse-star scalar
increment weighted by |q|^2 and the increment of the annealed upper-left
quadratic form.
Nonnegativity of the mean defect at every integer scale. This is the left-hand inequality of the ABK26 Step-2 display: the annealed inverse-star scalar of the cutoff is nonincreasing along the integer cube scales.
ABK26 Step 2 with a general load. For every integer pair of cube
scales n <= m and every load (p, q),
(shom_{L,*}^{-1}(cu_n) - shom_{L,*}^{-1}(cu_m)) |q|^2 <= 2 E[J(cu_n, p, q; a_L) - J(cu_m, p, q; a_L)].
This is the load-general form of the printed display: no rescaling of the load directions is needed, because the annealed coarse-grained identity is exact.
ABK26 Step 2, normalized display. Under the load normalization
e.pq.normed the squared norm |q|^2 = shom_L is positive, and the mean
defect obeys
0 <= shom_{L,*}^{-1}(cu_n) - shom_{L,*}^{-1}(cu_m) <= 2 |q|^{-2} E[J(cu_n, p, q; a_L) - J(cu_m, p, q; a_L)]
for every integer pair of cube scales n <= m.
Step 2, part (i): sign and monotonicity of the mean response #
The two facts the squaring step needs about the mean response itself: it is
nonnegative at every scale (e.Jenergyv.nosymm, in the mean), and it is
nonincreasing along the integer cube scales (e.subaddJ.nosymm).
Nonnegativity of the mean response. The response functional is pointwise nonnegative, hence so is its expectation, at every integer cube scale and every load.
The subadditivity chain of ABK26 Step 2. The mean response of the
genuine coefficient cutoff is nonincreasing in the cube scale, at every pair of
integer scales n <= k and every load. Applied at n = L this is the
inequality E[J(cu_n,p,q;a_L)] <= E[J(cu_L,p,q;a_L)] for L <= n.
Step 2, part (ii): the one-cube bound under the moment premise #
The one-cube bound. Under the proposition's fourth-moment premise
e.moment.bound.onmathcalE and the load normalization e.pq.normed, the mean
response of the genuine coefficient cutoff on its own cube obeys
E[J(cu_L, p, q; a_L)] <= delta_1.
The route is the first inequality of e.mathcalE.monotone.ordered at the
cutoff cube -- the a.e. domination
J(cu_L, shom_L^{-1/2} e, shom_L^{1/2} e; a_L) <= E_{s,infinity,2}(cu_L; a_L, shom_L)^2 in every unit direction -- followed by
Cauchy--Schwarz. The universal constant of the printed bound is therefore
1 here.
Step 2, part (iii): the squared means-downscale-by-defect display #
ABK26 e.means.downscale.by.defect (closed). Under the proposition's
fourth-moment premise e.moment.bound.onmathcalE with delta_1 in (0, 1/2]
and the load normalization e.pq.normed, for all integer cube scales L <= n <= m,
|shom_{L,*}^{-1}(cu_m) - shom_{L,*}^{-1}(cu_n)|^2 <= 4 shom_L^{-2} delta_1^2.
The universal constant is the explicit numeral 4. The proof chains the
normalized propagation display above (whose gauge is already |q|^{-2} = shom_L^{-1}) with E[J(cu_m,p,q;a_L)] >= 0, the subadditivity chain
E[J(cu_n,p,q;a_L)] <= E[J(cu_L,p,q;a_L)] at L <= n, and the one-cube bound;
the printed step shom_{L,*}^{-1}(cu_m) <= 2 shom_L^{-1} is not used.