High-contrast homogenization: Entry.Response.Kernel.DiagonalDefectCarriers #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Carriers of the diagonal weak-norm defect #
This file defines the average and cell defects weakAverageDefect, weakCellDefect and their
finite sums, and the pathwise optimizer energy weakOptimizerEnergy, of the diagonal weak-norm
estimate p.response.transfer, and proves the closed helper identities relating a cell average of
the doubled optimizer field to the block response mean. It also settles the degenerate-metric
branches of the estimate's primal bound, where the underlying block matrix fails to be a unit, and
records the real-arithmetic geometric-weight comparison and tail-weight selection used at the
branch cutoff M = 1.
HC bridge II: carriers and closed helpers for the diagonal weak-norm bound #
Carriers and closed helpers for the diagonal weak-norm estimate of the paper
p.response.transfer, depending only on ScaleAverageSeminorm.lean.
Carriers: the two finite sums and the pathwise optimizer energy. #
Index convention: the absolute-scale carriers are indexed by the scale k : ℤ, over the aligned
index set alignedIndex q k t; the grid carriers used here are indexed by the DEPTH n : ℕ below
t, over triadicIndexBox d n (ResponseBlockObjects.lean), exactly as besovSeminorm
and respAllScaleMax already are. So k = t - n throughout, and
alignedIndex q (t-n) t ↦ triadicIndexBox d n.
The recent cell defect C_{k,t}(E) at depth n (scale k = t - n). The root-mean-square,
over the 3^{nd} scale-(t-n) subcells of U_t, of the E-normalized difference between the
cell's coarse block and the coarse block of U_t.
The size carrier is the TWO-SIDED ‖E^{-1/2} D E^{-1/2}‖, written here as
‖toFullBlockMat (normalizedBlock D E)‖. The one-sided blockSpecBound (normalizedBlock D E)
controls only the upper spectral side and CANNOT carry the pointwise cell step: with E = I₁₈,
D = diag(-1, 1/17, …, 1/17) (d = 9), blockSpecBound (normalizedBlock D E) = 1/17 while
|D e₁| = 1 > 16/17, so even the explicit constant 16 does not repair it. blockSpecBound
remains correct for respAllScaleMax (ResponseBlockObjects.lean), which is the spectral
positive part
of p.response.transfer; the recent cell differences are bounded in their FULL norm at
p.response.transfer.
The defect is built from the coarse blocks of the RECENTRED field b (b = respCoeffMinus F a
at the call site) and normalized by the congruenced E = respEhatMinus; mixing the uncongruenced
numerator coarseBlock … a with the congruenced denominator is not the fixed-congruence invariant
carrier of p.response.transfer.
The sum avsum (WeakNorm.lean) is spelled out as (card)⁻¹ * ∑, as besovSeminorm does.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The recent averaged normalized defect D_{k,t}(E) at depth n (scale k = t - n). The flat
average over the scale-(t-n) subcells of U_t of the E-normalized cell-minus-U_t block
differences, taken entrywise through toFullBlockMat.
The defect is built from the recentred field b, normalized by the congruenced E, as in
weakCellDefect.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The recent cell sum 𝒰_cell, the 3^{-n/2}-weighted sum of the recent cell defects over
the finite window n ≤ H, at the exponent s = 1/2.
Finset.range (H+1) includes both endpoints.
Equations
- HCPolySupport.HighContrast.Multiscale.weakCellSum q t H E b = ∑ n ∈ Finset.range (H + 1), 3 ^ (-(↑n / 2)) * HCPolySupport.HighContrast.Multiscale.weakCellDefect q t n E b
Instances For
The recent averaged-defect sum 𝒰_av, the 3^{-(1/2 - rho/2)n}-weighted sum of the square
roots of the sizes of the averaged recent defects over the finite window n ≤ H, at s = 1/2.
The inner size is the TWO-SIDED norm of D, here ‖toFullBlockMat D‖; the one-sided
blockSpecBound D suffers the same loss as in weakCellDefect.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pathwise normalized optimizer energy
ℰ_t = (2 J_t)^{1/2} = ‖symm(b)^{1/2}∇v‖_{L_underlined²(U)}
(p.response.transfer). CoarseGraining's variationEnergyValue (Book/Ch02/Response.lean)
needs a Domain d together with a CoeffOn of it and a Solution, none of which the binders here
carry (they carry a bare Set (Vec d) and an AHarmonicFunction). The integrand is therefore
written directly: ∇v · symm(b) ∇v = ∇v · b ∇v = (X x).1 · (X x).2 for the doubled optimizer
field X = optimizerField b u (ResponseBlockObjects.lean), so this is the same real number.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Helpers. The pointwise comparison identity in the current carriers, the mean identity #
generalized off the centred cell, child-maximizer existence on every aligned subcell, and the nonnegativity facts.
The child-minus-parent mean difference is the reflected action of the block defect.
The mean identity on a general open bounded convex domain of positive volume.
The mean identity for a field that is only a.e. equal to an elliptic representative.
The mean identity for the recentred field a_- on an arbitrary aligned adapted cell.
The mean identity for the recentred field a_- on the centred cell U_t.
POINTWISE COMPARISON, identity half. The child-cell minus parent-cell optimizer mean
difference is exactly the reflected action of the coarse-block defect that weakCellDefect
normalizes.
Nonnegativity of the recent cell sum.
Nonnegativity of the recent averaged-defect sum.
The swap block exchanges the two slots.
Conjugating the metric block M_0 = diag(m, m^{-1}) by the swap R inverts it:
R^t M_0 R = diag(m^{-1}, m). This is the step that turns the reflected mean difference
R D x of the pointwise comparison into the M_0^{-1} quadratic form.
The degenerate metric branches of the diagonal weak-norm primal bound #
The binders of diagonalWeakNorm_primal_le
(DiagonalWeakNormBound.lean) give an ARBITRARY F : BlockMat d, so neither
(explicitCanonicalMetric F).PosDef nor (toFullBlockMat (respM0 F)).PosDef is available, while
the pointwise cell-defect estimates were stated with both. The degenerate branches are
settled WITHOUT a statement change, by showing that they are harmless.
This file does the metric half of that, from the bottom up: it identifies exactly which junk
value matSqrt (HCPoly/Setup/BlockAlgebra.lean) returns in each degeneration of
respM0 F = diag(m, m⁻¹), m = explicitCanonicalMetric F
(HCPoly/Entry/Setup/ProjectiveDistance.lean).
The structural fact that makes the classification finite is that explicitCanonicalMetric F is the
Mathlib inverse of a matrix, so it is EITHER a unit OR literally 0 — there is no
"singular but nonzero" metric. Hence exactly three branches:
ma unit andtoFullBlockMat (respM0 F)positive definite — the nondegenerate branch, the one the pointwise cell-defect estimate already covers;m = 0— thentoFullBlockMat (respM0 F) = 0andblockSqrt (respM0 F) = 0, so the left-hand side of the diagonal weak-norm bound is identically0;ma unit buttoFullBlockMat (respM0 F)NOT positive definite (equivalently: not positive semidefinite, since a unit PSD matrix is PosDef) — thenmatSqrtfalls through on BOTHrespM0 Fand its inverse, soblockSqrt (respM0 F)is the identity andnormalizedBlock E (respM0 F)isEitself. The metric simply disappears from both sides, and the cell step becomes its ownM_0 = Iinstance.
These degenerations are self-consistent, and the lemmas below establish that fact.
With an explicit hypothesis hm : m.PosDef on the metric, these branches cannot arise; they are
exactly the cost of the binder-free carrier map respM0 F.
The two junk values of matSqrt #
matSqrt M is the junk value 1 as soon as M is not positive semidefinite: a
positive semidefinite B with B * B = M would exhibit M = Bᴴ * B as positive semidefinite.
matSqrt 0 = 0.
matSqrt 1 = 1, the nondegenerate companion of the previous result.
The dichotomy of the canonical metric #
explicitCanonicalMetric F is a Mathlib matrix inverse, so it is either invertible or
literally 0: there is no "singular but nonzero" canonical metric. This is what makes the
degenerate classification finite.
When the canonical metric degenerates, the entire metric block does.
blockSqrt of a vanishing metric block vanishes.
Consequently every M_0^{1/2}-transported vector vanishes, so the left-hand side of the
diagonal weak-norm bound is identically 0 in this branch.
The indefinite branch: the metric disappears from both sides #
If the metric block is not positive semidefinite, blockSqrt (respM0 F) is the junk
identity, so M_0^{1/2} acts trivially on the left-hand side of the diagonal weak-norm bound.
In the same branch the INVERSE metric block is not positive semidefinite either, as
soon as the metric is a unit, so normalizedBlock E (respM0 F) is E itself: the printed
constant K_0 degenerates to ‖E‖ and nothing is lost.
Invertibility and the metric restriction on the unit branch #
The explicit left inverse of the flattened metric block on the unit branch. This is
the computational core of the metric inverse lemma (toFullBlockMat_respM0_inv,
DiagonalWeakNormBound.lean), isolated here because it needs only IsUnit of the metric
determinant, not positive definiteness.
Hence on the unit branch the flattened metric block is invertible, with NO positivity assumption whatsoever.
The canonical metric inherits positive semidefiniteness from the flattened metric block: restrict the quadratic form to the first slot.
The Ehat degeneration #
The OTHER degenerate side is the one where the congruenced annealed block
Ehat_t^- = respEhatMinus P jStar F t is singular; the statements recorded here do not close it.
The load collapse, one sub-case of the Ehat degeneration #
If respEhatMinus is singular then respLsqMinus = 0 forces the loads to vanish. That is TRUE
in the sub-case where the degeneration sits in the lower-right block of the annealed mean — but
only there; the remaining sub-case resists.
The bad-branch weight arithmetic of the cell-average estimate #
On the event {M > 1} of the all-scale maximum M, the cell-average estimate is absorbed by
its tail term, and the only remaining input is the geometric comparison of the weights
3^{-a j}. This file records that comparison as plain real arithmetic: a geometric series with
ratio 3^{-a}, the reciprocal bound (1 - 3^{-a})^{-1} ≤ 3/a on 0 < a ≤ 1, its value
(1 - 3^{-1/2})^{-1} ≤ 3 at a = 1/2, and the assembled bad-branch weight bound in terms of the
response parameters Quenched.contrastAlpha and Quenched.contrastRho.
The tail weight of the cell-average estimate, both branches at once #
The cell-average estimate e.response.weak.estimate prints its older-scale tail weight as a
single if at the cutoff 1: the branch 1 < M contributes the recent-scale value √M, and its
complement the older-scale weight 3^{-(Quenched.contrastAlpha γ * H)}. The two branches are
discharged by
different lemmas elsewhere in the development; this file packages the case split once and for all,
so that a consumer carrying M need not first decide which branch it lies on.
The branch-free tail comparison behind e.response.weak.estimate: a value Agood bounded by
cgood times the older-scale weight on M ≤ 1, and a value Abad bounded by cbad times √M
on 1 < M, are together dominated by max cgood cbad times the printed if tail weight.