High-contrast homogenization: Entry.Response.Kernel.DiagonalWeakNormAssembly #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Assembly of the diagonal weak-norm estimate #
This file assembles the diagonal weak-norm estimate of the response-transfer proposition
p.response.transfer from its two halves, the weakCellSum and weakAverageSum bounds, adding
the hypothesis pair the underlying statement omitted and recording the resulting bound at the
estimate's own carriers. Alongside it sit the adjoint twin of the averaged-defect window sum,
sharing the good-branch coefficient √2 (1 + √M · 3^(ρn/2)); the recent-scale decomposition
restricted to the depth-n triadic index box and its window sum; and the coincidence, for the
adjoint response, of the normalized block's one-sided spectral bound with its operator norm at a
positive definite pair.
The averaged-defect window sum for the adjoint sample #
This is the plus twin of the averaged-defect window sum weakAverageSum_half_le. The
per-scale bound on the abstract family A : ℕ → ℝ is the same good-branch coefficient
√2 (1 + √M · 3^{ρ n/2}), and the window summation is the same arithmetic on the geometric
weights 3^{-n/2} and 3^{-(1/2 - ρ/2)n}. The only change is the sample: the recentred field
a_- = respCoeffMinus F a and the response matrix E_-^t = respEhatMinus P jStar F t are
replaced by their adjoint counterparts a_+ = respCoeffPlus F a and
E_+^t = respEhatPlus P jStar F t. This is the averaged-defect summand of the weak-norm
estimate e.response.weak.estimate.
e.response.weak.estimate, averaged-defect window sum for the adjoint sample. For the
adjoint sample a_+ = respCoeffPlus F a, the adjoint response matrix
E_+^t = respEhatPlus P jStar F t, and a family A : ℕ → ℝ bounded per scale by the
good-branch coefficient √2 (1 + √M · 3^{ρ n/2}) against the averaged recent-defect size
‖weakAverageDefect · E_+^t · a_+‖, the 3^{-n/2}-weighted sum over the window n ≤ H is
bounded by 4 K L times the printed weighted averaged-defect sum
∑ 3^{-(1/2 - ρ/2)n} ‖weakAverageDefect · E_+^t · a_+‖.
M = respAllScaleMax P γ jStar F t a is assumed at most 1 (the nondegenerate branch), K and
L are nonnegative, and _hE records that the adjoint response matrix E_+^t is positive
definite; the latter is the nondegeneracy condition carried by the route.
The recent-scale decomposition with box-restricted integrability #
The recent-scale decomposition compares the normalized root-mean-square, over the depth-n
triadic cells, of the transported and recentred parent cell averages with the corresponding child
average plus the average of the parent-minus-child difference. Its conclusion sums only over the
cells indexed by triadicIndexBox d n, and its window sum only over n ≤ H, so the
integrability of the fields is needed only on those cells: a cell index outside the box is never
averaged.
This module restates the decomposition with that restricted hypothesis, which is the form the
optimizer field can actually supply, since the parent field is L² only on the adapted region
U.
The recent-scale decomposition at one depth, with box-restricted integrability. At depth
n, the head term of the actual family — the normalized root-mean-square over the triadic cells
of the transported, recentred parent cell averages — is at most the corresponding child term plus
the average-defect term, assuming the componentwise integrability of the parent and child fields
only on the triadic cells indexed by triadicIndexBox d n.
The recent-scale decomposition summed over the window, with box-restricted integrability.
The depth-n decomposition summed over n ≤ H against the 3^{-n/2} weights, assuming the
componentwise integrability of the parent and child fields only on the triadic cells indexed by
triadicIndexBox d n for each n in the window.
Assembly of the diagonal weak norm estimate #
This file assembles the estimate diagonalWeakNorm_primal_le
(DiagonalWeakNormBound.lean) from its two halves. It adds declarations only and restates
or weakens none of them.
What this file is for #
The statement omitted the hypothesis pair (hE : IsSymmetricBlockMat E) (hEpd : BlockPosDef E)
that the printed argument carries at the route's energy estimate. Here the surviving gap is
exactly (toFullBlockMat (respEhatMinus P jStar F t)).PosDef, and that gap is dischargeable,
as established in RecentHeadDefectHalves.lean, from RespCalibrated together with
RawOutput.symm and RawOutput.pos. This file chains those discharges into the context of
diagonalWeakNorm_primal_le rather than leaving them standing alone.
The results fall into three groups.
- The first concerns the maximum: the real-valued
respAllScaleMax(ResponseBlockObjects.lean) is a baresSup, which on an unbounded set takes Lean's junk value0; an explicit finiteness hypothesishfinite : diagonalWeakMaximum … ≠ ⊤excludes that. An envelope constant — precisely whatpathwise_envelope(WeakEstimateAssembly.lean) delivers almost everywhere — makes the defining setBddAbove, and the membership inequality thathfinitewas there to license follows. - The second concerns the mismatch between the two spectral quantities: the
weakCellSumhalf concludes against√‖toFullBlockMat (normalizedBlock Ê M₀)‖, whereas the statement prints√(blockSpecBound (normalizedBlock Ê M₀)), andblockSpecBound N ≤ ‖toFullBlockMat N‖is the wrong direction. Under the positive-definiteness condition the two are equal, becausenormalizedBlock Ê M₀is then positive definite, so the half can be restated on the printed quantity without touching the statement. - The third composes the two halves into the printed first summand and reduces the remaining hypothesis to the two analytic facts on which it rests, recording what is still missing.
Every statement is proved here, on the carriers of this library. The positive-definiteness of
the normalized block is supplied by Annealed.normalizedBlock_posDef
(HCPoly/Entry/Annealed/Normalization.lean), and the boundedness result rests on the finite-maximum
branch of the real-valued maximum.
The positive-definiteness condition at the route's own binder bundle. #
The boundedness of the real-valued maximum. #
The boundedness. An envelope constant bounding every weighted spectral excess makes the
defining set of respAllScaleMax (ResponseBlockObjects.lean) bounded above. The hypothesis holds
almost everywhere: it is the third component of pathwise_envelope
(WeakEstimateAssembly.lean). This is the content, on a real-valued carrier, of the
finiteness hypothesis hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤ that an earlier statement
carried: without it sSup takes the junk value 0.
The weakCellSum half, on the quantity the printed statement uses. #
The key equality. On positive definite N and M the spectral positive part of
normalizedBlock N M is all of normalizedBlock N M, so the two quantities
blockSpecBound (normalizedBlock Ê M₀) and ‖toFullBlockMat (normalizedBlock Ê M₀)‖ coincide.
Annealed.normalizedBlock_posDef is HCPoly/Entry/Annealed/Normalization.lean; the hard half of
the
equality is blockSpecBound_eq_norm_of_posSemidef
(RecentEnergyMapSupport.lean).
The metric factor. The same equality at the carriers of diagonalWeakNorm_primal_le: the
K₀ of p.response.transfer as it is printed equals the K₀ used by the weakCellSum half.
The weakCellSum half on the printed quantity. weakCellSum_half_le
(RecentHeadDefectHalves.lean) with its conclusion moved from the two-sided
operator norm to the one-sided blockSpecBound used in DiagonalWeakNormBound.lean. The
statement of diagonalWeakNorm_primal_le is untouched; the change is licensed exactly by the
positive-definiteness condition, which is discharged above. Constant 1 against the printed
16.
Composition of the two halves into the first printed summand. #
The composition of the two halves, with the child-maximizer family produced before the
per-scale family. The earlier composition statement binds the per-scale family A and its
constraint hscale before producing the child-maximizer family V. The recent-scale
decomposition of the head term into the child term plus the average-defect family exhibits the
intended A — the average-defect family — and that family depends on V, so it cannot be
supplied to that statement at all: the ∃ V is under the ∀ A.
This declaration is that statement with ∃ V moved outside ∀ A. It is strictly stronger than
the earlier statement (the same V now serves every A), nothing is weakened, and the proof is
the earlier statement's own, since it already obtains V from the weakCellSum half
independently of A.
The composition of the recent-scale decomposition with the preceding result: the head of the
left-hand side built from the actual parent optimizer u — the field supplied by
h6a_besovSeminorm_recentred_eq and h6a_besovSeminorm_head_tail_le
(RecentEnergyMapSupport.lean) — is bounded by the entire first printed
summand 16 K₀ L⁻ (weakCellSum + weakAverageSum).
The earlier composition statement bounded a sum over the child maximizers plus an abstract A;
here the child maximizers are gone from the left-hand side and A is no longer abstract — it is
the explicit average-defect family, produced by the recent-scale decomposition together with V.
The only thing still assumed is hscale, now asked of that explicit family rather than of an
abstract one. This is precisely the analytic recent-average bound on the average-defect family,
which is not proved anywhere here. The integrability side conditions are the same ones the
recent-scale support lemmas already carry.
The composition of the preceding result with its remaining hypothesis replaced by the two
analytic facts it rests on. Its single remaining hypothesis hscale is replaced by a per-depth
per-cell energy family G satisfying:
hcell: the recent-difference metric-norm-squared bound, composed with the all-scale-maximum response bound; andhenergy: the recent-difference energy bound.
The reduction is scaleInput_of_analytic (CoarseBlockPerCellInput.lean).
Neither analytic fact is proved here: their root energy_map_metric_le
(…/Provider/Response/EnergyMap.lean) rests on a doubled-response / blockSharp sublayer
absent from both HCPoly/Entry/ and the CoarseGraining dependency. What this result
establishes is that
nothing else is missing between them and the entire first printed summand.
A side hypothesis hLsq : 0 ≤ respLsqMinus … is not needed: it is exactly the nonnegativity of
the quadratic form of the positive-definite respEhatMinus at respxMinus, supplied from hE by
blockVecDot_nonneg_of_posSemidef (RecentScaleEnergyRoute.lean). Dropping a
hypothesis is a strengthening; nothing in the conclusion moved.
The metric factor of the normalized response block, adjoint sign #
For a positive definite numerator and a positive definite normalizer, the spectral positive
part of the normalized block is the whole matrix, so its one-sided spectral bound coincides
with its operator norm. This file records that coincidence for the adjoint response
respEhatPlus, the sign that is paired with respxPlus in the weak-norm estimate: the
metric factor printed there equals the one delivered by the cell-sum half.
The spectral bound of the respEhatPlus-normalized response block equals its operator
norm, because both respEhatPlus P jStar F t and the normalizer respM0 F are positive
definite.