High-contrast homogenization: Entry.Annealed.ParentChildRecurrence #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Parent Child Recurrence #
The parent-child recurrence for the annealed block, the result of
p.fixed.geometry.parent.child.recurrence: the parent cell is partitioned into aligned
children, the matrix-square-root congruence bound is transported to each of them, the
bounded-window estimate supplies the children's moment membership, and the two printed
coefficients of the recurrence are assembled.
The aligned children of a parent adapted cell #
The paper partitions the parent adapted cell ⋄_{j+h}^q into
3^{dh} aligned children z + ⋄_j^q, z ranging over the physical centres
3^j q w ∈ 3^j q ℤ^d whose standard-cell counterpart lies in the parent's centred cube.
HCPoly.Entry.Annealed.AlignedSubdivision/MeanOrder build this over the index w : Fin d → ℤ
(via alignedCenterSet_finite_card, coarseBlock_aligned_parent_le); this file re-indexes it
over the physical centre z : Vec d as a Finset (Vec d), in the literal shape the averaging
statement's left-hand side takes after normalizedBlock is pulled through the finite sum.
The Finset of physical centres of the scale-j children inside ⋄_{j+hn}^q:
the image, under the aligned centre map adaptedCellCenter q j, of the (finite) index set of
HCPoly.Entry.Annealed.AlignedSubdivision.alignedCenterSet_finite_card.
Equations
Instances For
The aligned children set is nonempty: the index w = 0 is always aligned.
Every aligned child's centre lies in the aligned lattice 3^j q ℤ^d.
The re-indexed pathwise aligned parent/child order: the majorant is literally the
(Z.card)⁻¹-weighted average of the children's coarse response over the physical Finset
alignedChildren q j hn, matching the averaging statement's left-hand side shape after
normalizedBlock is pulled through the finite sum.
Every point of the coarse response of an adapted cell is pathwise positive semidefinite
(entrywise CG block positive-definiteness, Book.Ch02.BlockPosDef, transported through
posDef_toFullBlockMat): the a.e. positive-semidefiniteness the positive-gap argument needs
of its F.
The annealed identity: every aligned child, at any generation at or above jStar, has the
same annealed matrix as its parent's own generation-j adapted mean.
The aligned-children equal-weight average is in L^N(S_N): the "bounded-window estimate
gives the required integrability" sentence of p.fixed.geometry.parent.child.recurrence
(e.source.adapted.bound), applied
to each child and combined by Source.memLqSchatten_finset_sum. No membership premise is added
to any consumer; this is finiteness only.
The entrywise expectation of the actual aligned average is the child-scale mean.
Normalization transport #
p.fixed.geometry.parent.child.recurrence: the transport matrix is the product of the
child mean square root and the parent mean inverse square root. Its squared
L2 operator norm is exactly the normalized mean operator norm. The sharp
Schatten congruence bound and the actual mean order give the exponential
loss bound. Both means are proved positive definite before cancellation;
no integrability, positivity, or order premise is added to the recurrence.
Reproved matSqrt cancellation, generalized to any finite real carrier #
HCPoly.Entry.Geometry.GeometryUpdateBounds.matSqrt_mul_matSqrt_inv/matSqrt_inv_mul_matSqrt are
private and specific to Mat d; the congruence identity below needs both directions at
FullBlockMat d = Matrix (BlockCoord d) (BlockCoord d) ℝ, a different carrier. Reproved here,
generalized to any finite index type, rather than reaching into that file's private
namespace.
Group 3 item 1: the deterministic congruence identity #
The change-of-normalization congruence identity, for every block X, given both adapted
means positive definite: a deterministic matrix identity, no probabilistic hypothesis.
Group 3 item 2: the operator-norm identity #
‖B‖² = |P^q_{j,j+h}|: the square of the transport matrix's operator norm is exactly the
operator norm of the transported normalized mean, via the C⋆-identity ‖BᵀB‖ = ‖B‖² (an
equality, not merely the fallback inequality).
Change normalization using the exact operator norm of the transport matrix.
Transport between ordered actual means costs at most the exponential determinant loss.
The parent–child recurrence #
Near p.fixed.geometry.parent.child.recurrence. The aligned children supply the actual average,
its expectation and order. Matrix averaging at the child normalization,
sharp normalization transport, and the positive-gap estimate give
the recurrence with the two printed coefficients. The ordered-mean
analysis supplies the full trace/determinant estimate and nonnegative loss.
All moment membership and both mean positive-definiteness proofs are derived from the standing law. The helper with an averaging premise is discharged by the ordinary endpoint here and by the exact averaging result. The latter returns the very same source constant and passes its threshold premise straight through.
Full coordinates preserve block subtraction.
Deterministic normalization is linear in the matrix being normalized.
Centering commutes with a nonempty equal-weight full-matrix average.
Pull normalization and centering through the actual finite average.
Actual expectation commutes with normalization when every entry is integrable.
The parent-normalized mean trace gap is bounded by the printed exponential term.
Normalization preserves the block order, with a genuine positive normalizer.
Normalization preserves positive semidefiniteness in the block order.
Assemble the recurrence from the actual averaging inequality on the aligned children. The averaging input is discharged by the ordinary endpoint below and by the exact averaging result.