High-contrast homogenization: Provider.Recurrence.PositiveGapClosure #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The positive-gap estimate read at the carriers of the fixed-grid recurrence #
l.fixed.geometry.positive.gap is proved for abstract random blocks: a positive excess D
caught below G_hat = P + Y, a bound b on the mean of tr D, and the mixed norms
x = ‖D‖_{L^Q(S_Q)}, y = ‖Y‖_{L^Q(S_Q)}. Three passages carry it onto the
data of p.fixed.geometry.parent.child.recurrence, and they are taken here.
The expectation identities. With F̂ the response over the parent cell and
G_hat the average of the responses over its aligned children, both normalized by
the parent mean E_p^q, the reference proof records E[D] = B and
E[tr D] = b for D = G_hat - F̂ and B = P_{j,p}^q - I. Both are the
interchange of a fixed linear functional with the block-valued Bochner integral:
normalization is a two-sided multiplication by a deterministic matrix and the
trace is a linear functional, so each passes through. The mean of the
normalized parent response is the identity and the mean of the normalized
average is the relative mean, so E[D] = P_{j,p}^q - I. Since D is positive
along every realization, the L^1 norm of tr D is its mean, which is the
fail-closed form the integrated trace-power display takes as its gap hypothesis.
The finiteness read-back. The integrated display is an inequality in
ℝ≥0∞. On the event that the two mixed norms are finite it becomes the
printed quadratic inequality between real numbers, and the two constants it
carries are reconciled into the single constant C = 2^{Q-2}(2m)^{1-1/Q} the
absorption step takes, at the cost of (2m)^{1-1/Q} ≥ 1.
The mixed-norm triangle step. The closing estimate of l.fixed.geometry.positive.gap is
pointwise; the conclusion is between mixed norms. Passing between them costs
the L^Q norm of a constant, which is that constant exactly because the law is
a probability measure — the one place in the chain where the normalization of
the law is genuinely used.
Flattening the block difference and the normalized difference #
The flattening of a difference of doubled blocks is the difference of the flattenings.
The flattening of the F-normalized difference, expanded as the difference
of the two congruences.
Entrywise integrability of a block-valued map #
The identity, read as a continuous linear map from the coordinatewise
(finite-product) presentation of FullBlockMat d into the matrix type itself.
Continuity is automatic on a finite-dimensional space; the map exists only to
move Bochner-integral values between the two topologically identical but
differently normed presentations FullBlockMat d carries — the Loewner-order
one open in this file and the coordinatewise one the generic product API
uses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trace against the block-valued integral #
The trace passes through the block-valued Bochner integral, being a linear functional on a finite-dimensional space.
The trace of an integrable block-valued map is integrable.
E[tr D] = b, fail-closed. For a block that is positive along every
realization the L^1 norm of its trace is the mean of that trace, with no
finiteness hedge: the trace is already nonnegative, so no absolute value is
lost. This is the form the gap hypothesis of the integrated trace-power display
is stated in.
The expectation identities at the adapted means #
The normalized excess is Bochner integrable as soon as the two responses are.
0 ≤ D. The excess of the aligned average over the response is
positive along every realization, congruence by the inverse square root of the
parent mean preserving the pathwise order.
E[D] = B (l.fixed.geometry.positive.gap, at the carriers of
p.fixed.geometry.parent.child.recurrence): the mean of the normalized excess of the aligned
average over the parent response is P_{j,p}^q - I. The parent response
integrates to the parent mean, whose normalization by its own inverse square
root is the identity, and the aligned average integrates to the child mean,
whose normalization is the relative mean.
E[tr D] = b (l.fixed.geometry.positive.gap, at the carriers of
p.fixed.geometry.parent.child.recurrence): the mean of the trace of the normalized excess
is the trace gap tr(P_{j,p}^q - I) of the relative mean.
The gap hypothesis of the integrated trace-power display, at the adapted
means. The L^1 norm of the trace of the normalized excess is the trace gap
of the relative mean, so any bound on that gap is a bound in the fail-closed
form the display consumes.
The finiteness read-back of the quadratic display #
The extended-real display, read back on finite mixed norms. A bound
u^Q ≤ αb + β(y^{Q-1}x) in ℝ≥0∞ between the images of nonnegative reals is
that bound between the reals themselves, ENNReal.ofReal being an order
embedding on the nonnegative axis.