High-contrast homogenization: Entry.Response.Kernel.RecentHeadDefectHalves #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The two halves of the recent-head defect bound #
This file proves the two halves the diagonal weak-norm estimate's recent head is built from, for
the response-transfer proposition p.response.transfer: the weakCellSum half, bounding the
normalized root-mean-square of the child-optimizer mean defects by the reflected coarse-block
defect action, with the pointwise cell-defect step discharged of its metric-nondegeneracy
hypotheses; and the weakAverageSum half, the per-scale window sum over the good-branch
coefficient √2 (1 + √M · 3^(ρn/2)). Both halves record, along the way, that the branch where
the response matrix respEhatMinus P jStar F t is singular never occurs, since every
diagonalWeak*-family lemma excludes it by hypothesis.
HC bridge II, the recent-head cell-defect package #
The pointwise cell-defect step, its form with the metric nondegeneracy hypotheses
discharged, and the full weakCellSum half of the recent head.
HELPERS. The POINTWISE CELL-DEFECT step of the recent head: #
the first of the two summands of the printed right-hand side. The per-cell input is
metricNormSq_blockAverage_sub_adapted_le (DiagonalWeakNormComparison.lean), and
diagonalWeak_recent_cell_bound is the cell bound.
The identity cellAverage_optimizerField_respCoeffMinus_sub_eq
(DiagonalDefectCarriers.lean) identifies the child-minus-parent optimizer
mean difference with R D x, where D is the coarse-block defect that weakCellDefect
normalizes and x = (-p, q^-) is the response load; the reflected M_0
metric of that vector becomes the M_0^{-1} quadratic form, and the matrix comparison closes
the estimate. The lemmas below are the links between them.
The identity cellAverage_optimizerField_respCoeffMinus_sub_eq and its dependency chain, plus
blockMatVecMul_blockSwap and blockVecDot_blockSwap_respM0, are public in the support file
and are used directly below.
The block diag(m^{-1}, m) is exactly the inverse of the
flattened metric block M_0 = diag(m, m^{-1}). This is what lets the matrix comparison
be applied with M = M_0, so that its metric constant is the printed
K_0 = |M_0^{-1/2} Ehat M_0^{-1/2}|.
POINTWISE CELL DEFECT. The metric length of the reflected action M_0^{1/2} R D x
of a block defect D on a response load x is controlled by the metric factor
K_0 = |M_0^{-1/2} E M_0^{-1/2}|, the squared E-normalized size of D — which is exactly the
summand of weakCellDefect — and the E-quadratic load x. E x = (L^-)^2. Composed with
cellAverage_optimizerField_respCoeffMinus_sub_eq this is the current-carrier form of
metricNormSq_blockAverage_sub_adapted_le.
WITHOUT THE METRIC NONDEGENERACY BINDERS. #
DiagonalDefectCarriers.lean classifies respM0 F for an ARBITRARY F. There are
exactly three branches, and in each of them the pointwise cell-defect bound holds with the SAME
printed constants — so the pointwise estimate can be used
with hm and hM0 DISCHARGED, not assumed. The part of the classification that concerns
explicitCanonicalMetric / respM0 is settled here; the respEhatMinus part is NOT settled
here.
The pointwise cell-defect bound holds for
EVERY F : BlockMat d, with no hypothesis on explicitCanonicalMetric F or on respM0 F.
explicitCanonicalMetric F = 0:blockSqrt (respM0 F)annihilates everything, so the left side is0and the right side is a product of nonnegative factors.explicitCanonicalMetric Fa unit andrespM0 Fpositive semidefinite: thenrespM0 Fis positive DEFINITE (Matrix.PosSemidef.posDef_iff_isUnit) andexplicitCanonicalMetric Fis too, so this is literally the estimate withhmandhM0.explicitCanonicalMetric Fa unit andrespM0 Fnot positive semidefinite:matSqrtfalls through on bothrespM0 Fand its inverse, soM_0^{1/2}acts as the identity and the printed metric factor is‖Ehat‖itself; the bound is then the matrix comparison atM = I.
The normalized finite-cell root-mean-square form of
the pointwise estimate; same proof, with hm/hM0 discharged instead of assumed.
weakCellDefect form of the normalized finite-cell root-mean-square estimate.
THE weakCellSum HALF OF THE RECENT HEAD. #
With the identity cellAverage_optimizerField_respCoeffMinus_sub_eq
(DiagonalDefectCarriers.lean) available, the
child-cell mean defect is EXACTLY the reflected coarse-block defect action that
the pointwise estimates bound, at the response load x^- = (-p, q^-) (ResponseBlockObjects.lean).
The associated estimates are diagonalWeak_recent_cell_bound
(DiagonalWeakNormRecentCell.lean) and the first summand of
diagonalWeak_recent_scale_decomposition_le (DiagonalWeakNormRecentDecomposition.lean).
The weakCellSum half, at one depth. The normalized finite-cell root-mean-square
of the depth-n CHILD-OPTIMIZER mean defects, measured in M_0, is bounded by
sqrt K_0 * L^- * weakCellDefect q t n Ehat a_-, with constant 1 against the printed 16.
THE weakCellSum HALF OF THE RECENT HEAD, all depths. Choosing the child
maximizers simultaneously and summing the one-depth estimate against the printed 3^{-n/2}
weights over the window n <= H produces EXACTLY weakCellSum, with constant 1 against the
printed 16. The first summand of diagonalWeak_recent_scale_decomposition_le
(DiagonalWeakNormRecentDecomposition.lean) is the corresponding estimate.
The weakAverageSum half of the diagonal weak-norm bound and the nondegeneracy discharge #
The nondegeneracy discharge #
In the branch where respEhatMinus P jStar F t is singular, the diagonal weak-norm statement
(DiagonalWeakNormBound.lean) is equivalent to its left-hand side being exactly 0.
That branch is never proved: every diagonalWeak* lemma excludes it, by the pair
of binders (hE : IsSymmetricBlockMat E) (hEpd : BlockPosDef E)
(DiagonalWeakNormPrimal.lean), and the
only junk branch anywhere near this material — canonFactor_exists
(Canonical.lean) — carries the docstring
"the junk value on non-positive data is never used". So the missing case is a DROPPED
HYPOTHESIS, not a missing proof.
The results below show that the dropped hypothesis is FREE at the consumers: the route's own
RespCalibrated Cc P jStar F s t (CenteredEnergyIdentity.lean) already contains
C⁻¹ M_0 ≤ Ehat_t^± in the Loewner order, and RawOutput.symm/RawOutput.pos
(ResponseBlockObjects.lean) already give (explicitCanonicalMetric F).PosDef, hence
(toFullBlockMat (respM0 F)).PosDef (LoadMeanIdentity.lean). Both binders are in scope at
respWeakEnergyOf_minus_le (WeakEstimateAssembly.lean) and at
response_weak_estimate_of_route (WeakEstimateAssembly.lean) already, so no statement text
changes. The satisfiability statement is in ∃ form.
The weakAverageSum half #
For the second printed summand, the estimate
diagonalWeak_recent_average_good_le (DiagonalWeakNormRecentBound.lean) feeds into
normalized_diagonalWeak_recent_head_le (DiagonalWeakNormRecentHead.lean). Its
per-scale analytic input — the energy map metricBlockNormSq_recent_difference_le
(DiagonalWeakNormRecentEnergyMap.lean) composed with the difference-energy bound
diagonalWeak_recent_difference_energy_le (DiagonalWeakNormRecentQuadratic.lean) — has
no counterpart in this tree yet and is left as the explicit hypothesis hscale of
weakAverageSum_half_le.
Everything between that input and weakAverageSum is proved here:
the good-branch coefficient arithmetic √2 (1 + √M·R) ≤ 4R (avCoeff_le, cf.
DiagonalWeakNormRecentBound.lean), the weight identity W · R = 3^{-(1/2-ρ/2)n}
(recentWeight_mul, cf. DiagonalWeakNormRecentHead.lean), and the window
summation into weakAverageSum (weakAverageSum_window_le, cf.
DiagonalWeakNormRecentHead.lean).
CARRIER MAP (the section docstring of DiagonalWeakNormBound.lean is authoritative):
the source estimates use E ↦ respEhatMinus P jStar F t, m ↦ respM0 F,
q ↦ respGrid jStar F, s = 1/2, rho = Quenched.contrastRho γ, delta = 1, k = t - n. The
source carriers are ℝ≥0∞ with an
if diagonalWeakMaximum … = ⊤ then ⊤ else … guard; here everything is plain ℝ, so the guard
vanishes and the hfinite : diagonalWeakMaximum … ≠ ⊤ binder has no counterpart at all —
respAllScaleMax is real-valued by construction (ResponseBlockObjects.lean). The inner
size blockSize D (blockIdentity d) of the source carriers is this tree's
‖toFullBlockMat D‖
(DiagonalDefectCarriers.lean), which is why
blockSize_diagonalWeakAverageDefect_nonneg
(DiagonalWeakNormComparison.lean) — one of the five leaf consumers of hEpd — is here
just norm_nonneg and needs nothing.
The dropped hypothesis and its discharge at the consumers. #
The weakAverageSum half, assembled. #
The analytic input feeding this assembly is
diagonalWeak_recent_average_bound
(DiagonalWeakNormRecentBound.lean), whose own inputs are the
energy map metricBlockNormSq_recent_difference_le
(…/DiagonalWeakNormRecentEnergyMap.lean) and the difference-energy bound
diagonalWeak_recent_difference_energy_le (…/DiagonalWeakNormRecentQuadratic.lean).
Neither has a counterpart in this tree; both appear here as the hypothesis hscale of
weakAverageSum_half_le.
rho = Quenched.contrastRho γ = (1+γ)/2 is positive on γ ∈ Set.Ico 0 1; this is
the side condition hrho : 0 < rho (…/DiagonalWeakNormPrimal.lean), discharged here
rather than assumed, exactly as the section docstring of DiagonalWeakNormBound.lean records.
The geometric weight R = 3^{rho(t-k)/2} at k = t - n is 3^{rho n / 2} ≥ 1,
the condition hR1 of diagonalWeak_recent_average_good_le
(…/DiagonalWeakNormRecentBound.lean).
The good-branch coefficient: √2 (1 + √M R) ≤ 4 R whenever M ≤ 1 and 1 ≤ R.
This is the content of the good branch for the averaged term, the condition hcoeff of
diagonalWeak_recent_average_good_le (…/DiagonalWeakNormRecentBound.lean), at
delta = 1 so that hgood : M ≤ delta and hdelta1 : delta ≤ 1 collapse into M ≤ 1.
The weight identity: W · R = 3^{-(s - rho/2) n} at s = 1/2, which is the
weakAverageSum weight of DiagonalDefectCarriers.lean, the condition hpow of
normalized_diagonalWeak_recent_head_le (…/DiagonalWeakNormRecentHead.lean).
The window summation: a per-scale bound against the printed weakAverageSum weight
sums over the window n ≤ H to exactly K L · weakAverageSum, the condition hsum of
normalized_diagonalWeak_recent_head_le (…/DiagonalWeakNormRecentHead.lean), whose
diagonalWeakAverageSum_eq unfolding is here the def itself.
The weakAverageSum half: diagonalWeak_recent_average_good_le
(…/DiagonalWeakNormRecentBound.lean) composed with the averaged branch of
normalized_diagonalWeak_recent_head_le (…/DiagonalWeakNormRecentHead.lean), on these
carriers at s = 1/2, rho = Quenched.contrastRho γ, delta = 1.
hscale is diagonalWeak_recent_average_bound
(…/DiagonalWeakNormRecentBound.lean) on these carriers; it is the only analytic input
and it has no counterpart here yet. hE is the positive-definiteness condition on
respEhatMinus P jStar F t, discharged at the consumers. Everything else — the good-branch
coefficient (avCoeff_le), the weight identity (recentWeight_mul), the window
summation (weakAverageSum_window_le) — is proved.
The hfinite : diagonalWeakMaximum … ≠ ⊤ binder has no counterpart: respAllScaleMax is
real-valued (ResponseBlockObjects.lean), so the ⊤ guard vanishes with it.
The all-scale-maximum bricks, stated carrier-free. #
These are the three arithmetic steps that turn the all-scale maximum into the
per-cell response size B = 1 + √M · 3^{rho n/2} used by hsize of
diagonalWeak_recent_average_bound
(DiagonalWeakNormRecentBound.lean). They are stated here on
bare reals, so they carry no E-nondegeneracy at all and are reusable for any carrier choice.
The step that is NOT carrier-free — ‖N‖ ≤ 1 + blockSpecBound (N - I) for
positive semidefinite N, the estimate blockSize_le_one_add_blockExcess
(…/DiagonalWeakNormMaximum.lean) — is NOT here: it needs blockSpecBound
subadditivity, which exists in this tree only as the private blockSpecBound_le_add
(WeakEstimateAssembly.lean), DOWNSTREAM of this file.
Removing the maximum's weight costs the reciprocal geometric factor, the estimate
blockExcess_le_mul_rpow_of_weighted_le (…/DiagonalWeakNormMaximum.lean), at
k = t - n so that t - k is n.
The square root inherits half the maximum's geometric weight, producing exactly the
√M · 3^{rho n/2} of B, the estimate
sqrt_blockExcess_le_sqrt_mul_rpow_of_weighted_le (…/DiagonalWeakNormMaximum.lean).
Composed with le_mul_rpow_of_weighted_le this is
sqrt_blockSize_adaptedResponse_le_of_maximum_finite
(…/DiagonalWeakNormMaximum.lean) up to the one non-carrier-free step named in the
section note above.