High-contrast homogenization: Entry.Response.Kernel.RandomToAnnealedRecentring #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The random-to-annealed recentring bound #
This file proves the analytic core of the recentring bound p.response.transfer: the flat
quadratic-form comparison bounding the metric size of the random cell average's deviation from its
annealed mean, and the resulting bound integral_respRecentre_sq_le_minus/_plus after
integrating over the coefficient law. It also completes, for the adjoint sample, the weakCellSum
half of the recent-head cell-defect estimate — the normalized root-mean-square of the
child-optimizer mean defects as the reflected coarse-block defect action of the adjoint
coefficient — and the adjoint twin of the per-scale analytic input, whose sign-free algebraic
spine is reused unchanged.
The recentring vector c_a in the self-dual metric #
The analytic core of the recentring bound (WeakEstimateAssembly.lean,
integral_respRecentre_sq_le_minus/_plus)
has three layers:
centered_metric_quadratic_le-- the flat quadratic-form comparison, the entire analytic content;metricBlockNormSq_responseAverage_sub_le/sqrt_metricBlockNormSq_responseAverage_sub_le-- its packaging through the mean identity;profilePrimalCenterVariance_le_variance-- the recentring bound, of whichrecentre_sq_le_minusandrecentre_sq_le_plusbelow are the pathwise half.
The eLpNorm/ℝ≥0∞ formulation of these bounds carries four extra carriers metricBlockNormSq,
blockSize, relSize, diagonalWeakMetricFactor/diagonalWeakLoadMinus, none of which this
tree has. The proof below therefore works in Bochner integrals and spells the carriers out in
this tree's own vocabulary:
| carrier | here |
|---|---|
metricBlockNormSq m v | blockVecDot (blockMatVecMul (blockSqrt (respM0 F)) v) (…) |
relSize E M | blockOpNorm (normalizedBlock E (respM0 F)) |
blockSize D E | blockOpNorm (normalizedBlock D E) |
diagonalWeakMetricFactor m E ^ 2 | respK0SqMinus P jStar F t (blockSpecBound!) |
diagonalWeakLoadMinus E p r ^ 2 | respLsqMinus P jStar F t e |
scaleVariance | respAllScaleAbs |
The one place the dictionary is not a rename is diagonalWeakMetricFactor ↦ respK0Sq±: the former
is an operator norm (relSize), while the latter is a blockSpecBound. They agree on a positive
semidefinite block, which is what blockOpNorm_le_blockSpecBound below supplies.
1. The flat quadratic-form comparison #
THE ANALYTIC CORE. The flat comparison centered_metric_quadratic_le, with the carrier
relSize E M written out as ‖M^{-1/2} E M^{-1/2}‖:
(D x) · M⁻¹ (D x) ≤ ‖M^{-1/2} E M^{-1/2}‖ · ‖E^{-1/2} D E^{-1/2}‖² · (x · E x).
Route: factor D = E^{1/2} B E^{1/2} with B = E^{-1/2} D E^{-1/2}, so
M^{-1/2} D x = (M^{-1/2} E^{1/2}) B (E^{1/2} x); apply vecSq_mulVec_le twice and read the
outer factor off the C*-identity ‖N‖² = ‖N Nᵀ‖ at N = M^{-1/2} E^{1/2}, where
N Nᵀ = M^{-1/2} E M^{-1/2}.
2. M_0 = diag(m, m^{-1}): symmetry, positivity, and its inverse #
R M_0 R = M_0⁻¹, in the flat picture: the inverse of M_0 = diag(m, m^{-1}) is
diag(m^{-1}, m), which is exactly the block blockVecDot_blockSwap_respM0
(DiagonalDefectCarriers.lean) produces from the swap conjugation.
3. blockOpNorm and blockSpecBound agree on a positive semidefinite block #
blockOpNorm N ≤ blockSpecBound N on a positive semidefinite block. The converse of the
unconditional blockSpecBound_le_blockOpNorm (WeakEstimateAssembly.lean); this is the one
place where positive semidefiniteness is genuinely needed, and it is what identifies this tree's
respK0Sq± (a blockSpecBound) with the carrier diagonalWeakMetricFactor ^ 2 (a relSize,
i.e. an operator norm).
4. The mean identity for the PLUS sign #
The mean identity for the recentred field a_+ on the centred cell U_t: the plus twin of
cellAverage_optimizerField_respCoeffMinus_eq (DiagonalDefectCarriers.lean),
which the tree did not have. The elliptic datum is the a.e.-representative one of
exists_elliptic_representative_respCoeffPlus (EllipticRepresentativeInputs.lean), so no
ellipticity
hypothesis is added.
5. THE PATHWISE RECENTRING BOUND #
The generic pathwise recentring bound. With x the load vector, Ehat the annealed
block and A the pathwise block, the recentring vector c = M_0^{1/2}(⟨X⟩ − Y) obeys
|c|² ≤ |M_0^{-1/2} Ehat M_0^{-1/2}| · ‖Ehat^{-1/2}(A − Ehat)Ehat^{-1/2}‖² · (x · Ehat x),
with the first factor replaced by its blockSpecBound, i.e. by K_0². This is the
blockVecDot/Bochner form of metricBlockNormSq_responseAverage_sub_le.
6. The two response instances #
The pathwise recentring bound, minus sign. Stated on the body of respRecentreMinus
(WeakEstimateAssembly.lean) and with respK0SqMinus (WeakEstimateAssembly.lean) spelled out,
because both live downstream of this file; at the consumer both are rfl.
The pathwise recentring bound, plus sign.
The weakCellSum half of the recent head for the adjoint sample #
This is the adjoint (a_+ = aᵗ + g) twin of the weakCellSum half of the recent-head
cell-defect estimate e.response.weak.estimate. The normalized finite-cell root-mean-square
of the child-optimizer mean defects is the reflected coarse-block defect action of the adjoint
coefficient a_+ = respCoeffPlus F a at the adjoint load x^+ = (-p, q^+); summing the
per-depth bound against the weights 3^{-n/2} over the window n ≤ H produces exactly
weakCellSum, with the printed prefactor
√‖M_0^{-1/2} Ê_+^t M_0^{-1/2}‖ · L^+.
The only inputs that are specialised to the recentred (minus) carriers are the two mean identities for the optimizer field; their adjoint counterparts are provided here. Every reflected-defect comparison it consumes is stated for a generic coefficient field, block and load, and so applies to the adjoint sample unchanged.
The adjoint optimizer-mean identities #
The adjoint twin of the optimizer-mean identity on an aligned adapted subcell: the cell
average of
the optimizer field for a_+ = aᵗ + g equals the block response mean of the coarse block matrix
at the adjoint loading (-p, r). The elliptic datum is the a.e.-representative one, so no
ellipticity hypothesis is added.
The adjoint pointwise comparison identity: the child-cell minus parent-cell optimizer mean
difference for a_+ = aᵗ + g is exactly the reflected action of the coarse-block defect that
weakCellDefect normalizes.
Adjoint child maximizer selection #
Child response maximizers for the adjoint coefficient can be chosen simultaneously at every depth and cell label.
The weakCellSum half for the adjoint sample #
e.response.weak.estimate, weakCellSum half, at one depth, for a_+. The normalized
finite-cell root-mean-square of the depth-n child-optimizer mean defects, measured in M_0, is
bounded by √K_0 · L^+ · weakCellDefect, where K_0 = ‖M_0^{-1/2} Ê_+^t M_0^{-1/2}‖ and
(L^+)^2 = x^+ · Ê_+^t x^+.
e.response.weak.estimate, THE weakCellSum HALF OF THE RECENT HEAD, for a_+. For the
adjoint sample a_+ = respCoeffPlus F a, the adjoint response matrix
E_+^t = respEhatPlus P jStar F t and the adjoint load x^+, choosing the child maximizers
simultaneously and summing the per-depth bound against the weights 3^{-n/2} over the window
n ≤ H produces exactly weakCellSum, with the printed prefactor
√‖M_0^{-1/2} Ê_+^t M_0^{-1/2}‖ · L^+.
The plus twin of the per-scale analytic input #
scaleInput_of_analytic_plus is the adjoint (a_+) twin of
scaleInput_of_analytic (CoarseBlockPerCellInput.lean): the per-scale input of
the cell-average lemma with the response sample replaced by respEhatPlus, respLsqPlus and
respCoeffPlus. The algebraic spine scaleInput_spine_le is sign-free and is reused
unchanged, so the two analytic inputs keep exactly the same shape with the plus sample.
The adjoint (a_+) twin of scaleInput_of_analytic.
The index set is triadicIndexBox d n, the root is blockSqrt (respM0 F), and the scalars are
the plus ones: √(blockSpecBound (normalizedBlock (respEhatPlus …) (respM0 F))), the all-scale
maximum factor 1 + √(respAllScaleMax …) · 3^{ρn/2}, √(respLsqPlus …), and the block size of
weakAverageDefect … (respEhatPlus …) (respCoeffPlus …). The per-cell hypothesis hcell and
the averaged energy hypothesis henergy are transported verbatim from the minus statement.