High-contrast homogenization: Entry.Response.Kernel.RecentScaleEnergyRoute

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The recent-scale decomposition, Loewner envelope and energy map

This file proves three steps of the response-transfer proposition p.response.transfer. The first is the recent-scale decomposition, writing the transported recentred parent cell average as the child average plus the parent-minus-child difference. The second is the Loewner envelope N ≤ ‖N‖ · I of a doubled block by its operator norm, needed for the quadratic half of the diagonal weak-norm estimate. The third is the coarse energy-map bound on the doubled response space, reached through two independent chains of metric comparisons and recorded together with the quadratic-form identities it rests on.

The recent-scale decomposition

Nothing here restates or weakens an existing declaration, and diagonalWeakNorm_primal_le (DiagonalWeakNormBound.lean) is untouched.

The decomposition

Between the compiled bound (DiagonalWeakNormAssembly.lean) and diagonalWeakNorm_primal_le lie three steps. This file is the first: the scale decomposition.

The compiled bound is ∑_{n ≤ H} 3^{-n/2} · (cellTerm V n + A n), where cellTerm V n is built from a per-cell CHILD maximizer V n w and A n is an abstract per-scale average-defect term. The left-hand side of diagonalWeakNorm_primal_le, after the two support lemmas (RecentEnergyMapSupport.lean), is the head of the seminorm of the ACTUAL family: the same expression with the PARENT field Xu in place of V n w. The recent-scale decomposition is what connects them, at each depth n and then summed:

headTerm n ≤ cellTerm n + defectTerm n,

with defectTerm n the normalized root-mean-square of the averaged parent-minus-child difference — i.e. it both supplies the inequality AND exhibits the witness for the bound's otherwise abstract A. What the bound then still assumes about that witness is the analytic per-scale bound hscale, which is NOT in this file.

The proof uses the two ingredients, on these carriers:

• averaging the child/parent difference is the difference of the cell averages; here cellAverage_sub.
• the split parent − mean = (child − mean) + (parent − child) followed by the triangle inequality in the normalized ℓ²(Z) of block vectors; here recentCell_split.

Two implementation notes:

1. The difference is taken as parent − child from the start, so no separate sign-cancellation step is needed.
2. The quantity is spelled inline as √(|Z|⁻¹ · ∑_{w ∈ Z} ⟪·,·⟫), matching weakCellSum and h6a_besovSeminorm_head_tail_le. The triangle inequality for it is normalized_blockL2_add_le (RecentEnergyMapSupport.lean).

Averaging a difference.

theorem HCPolySupport.HighContrast.Multiscale.cellAverage_sub {d : ℕ} {V : Set (Vec d)} (F G : Vec d → BlockVec d) (h1F : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).1 j) V MeasureTheory.volume) (h2F : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).2 j) V MeasureTheory.volume) (h1G : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (G x).1 j) V MeasureTheory.volume) (h2G : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (G x).2 j) V MeasureTheory.volume) : (cellAverage V fun (x : Vec d) => F x - G x) = cellAverage V F - cellAverage V G

The cell average of a difference is the difference of the cell averages. It is stated for arbitrary F, G rather than for two particular fields, with the componentwise IntegrableOn side conditions explicit, because the integrability of optimizerField on an adapted cell is supplied separately by the consumer (the same side conditions two earlier support lemmas already take, RecentEnergyMapSupport.lean). That makes it reusable and keeps the MemVectorL2 plumbing out of the decomposition.

R1-2. The split at one cell.

theorem HCPolySupport.HighContrast.Multiscale.recentCell_split {d : ℕ} {V : Set (Vec d)} (R : BlockMat d) (Xu Xv : Vec d → BlockVec d) (c : BlockVec d) (h1u : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (Xu x).1 j) V MeasureTheory.volume) (h2u : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (Xu x).2 j) V MeasureTheory.volume) (h1v : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (Xv x).1 j) V MeasureTheory.volume) (h2v : ∀ (j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (Xv x).2 j) V MeasureTheory.volume) : blockMatVecMul R (cellAverage V Xu - c) = blockMatVecMul R (cellAverage V Xv - c) + blockMatVecMul R (cellAverage V fun (x : Vec d) => Xu x - Xv x)

R1-2. The split at one cell. The transported, U_t-recentred cell average of the PARENT field is the corresponding quantity for the CHILD field plus the transported average of the parent-minus-child difference:

R·((Xu)_{V} − c) = R·((Xv)_{V} − c) + R·((Xu − Xv)_{V}).

This is the algebraic heart of the mine's hsplit (…/DiagonalWeakNormRecentDecomposition.lean), with the sign taken as parent − child so that the mine's separate blockAvsumL2_neg step is not needed.

R1-3. The decomposition at one depth.

R1-4. The decomposition summed over the window, the shape AS-9 consumes.

R3-1. The tail weight (node R3, partial).

The Loewner / operator-norm layer, on the block-matrix carrier

L-1 … L-5, proved here. Nothing restates or weakens any existing declaration, and the target diagonalWeakNorm_primal_le is untouched.

Why this module exists

quadratic_le_norm_normalizedBlock below — the quadratic half of the estimate — needs the Loewner envelope N ≤ |N| · I_{2d} of a doubled block by its operator norm. The proof of that step in HCPoly/Entry/Response/Kernel/OptimizerEnergyIdentity.lean (blockSpecBound_attained) is private and strictly downstream of this module, so it cannot be used here.

This module re-proves the step where it can be used: it imports only RecentScaleEnergyRoute, and is imported by CoarseBlockPerCellInput, so it sits strictly upstream of WeakEstimateAssembly. The original declarations are neither deleted nor made public.

Two corrections to the diagnosis

1. The step actually needed is NOT blockSpecBound_attained. That lemma concludes N ≤ blockSpecBound N · I and is about the sInf carrier; what is needed is the bound by the OPERATOR NORM, x · N x ≤ |N| (x · x), for an ARBITRARY (in particular not positive semidefinite — the averaged defect is a difference of coarse blocks) matrix. That is L-1 and L-2 here.
2. blockSpecBound_attained (HCPoly/Entry/Response/Kernel/OptimizerEnergyIdentity.lean) is a duplicate: blockSpecBound_attained_of_loewnerLE (HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean) is the same statement, and that module is upstream of this chain. It is private there too, so it is equally unusable, though its import direction is not the obstruction.

The analogous estimate is diagonalWeak_recent_response_quadratic_le (HCPoly/Provider/Response/DiagonalWeakNormRecentQuadratic.lean). Nothing is imported from it and no file is copied; the proof is reproduced on the block-matrix carriers, with its blockSize D (blockIdentity d) replaced by ‖toFullBlockMat ·‖, which is what weakAverageDefect and CH-3's henergy print.

Flat helpers

L-1 … L-3: the Loewner / operator-norm layer

theorem HCPolySupport.HighContrast.Multiscale.loewner_le_opNorm_identity {d : ℕ} (N : BlockMat d) : BlockMatLoewnerLE N (blockScale ‖toFullBlockMat N‖ (Book.Ch02.blockIdentity d))

L-2. The Loewner envelope of an arbitrary doubled block by its operator norm, N ≤ |N| · I_{2d}. It is proved here with no hypothesis on N at all.

theorem HCPolySupport.HighContrast.Multiscale.blockMatLoewnerLE_blockScale_blockSpecBound_self {d : ℕ} (N : BlockMat d) : BlockMatLoewnerLE N (blockScale (blockSpecBound N) (Book.Ch02.blockIdentity d))

L-3. blockSpecBound N attains its defining infimum, UNCONDITIONALLY: the set {c ≥ 0 | N ≤ c I} is never empty, because L-2 puts ‖toFullBlockMat N‖ in it. This re-proves blockSpecBound_attained (HCPoly/Entry/Response/Kernel/OptimizerEnergyIdentity.lean) and blockSpecBound_attained_of_loewnerLE (HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean), both private, and drops their (c : ℝ) (hc : 0 ≤ c) (h : BlockMatLoewnerLE N (blockScale c (blockIdentity d))) witness hypotheses, so it is strictly stronger than either.

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_nonneg_of_posSemidef {d : ℕ} (A : BlockMat d) (hA : Matrix.PosSemidef (toFullBlockMat A)) (X : BlockVec d) : 0 ≤ blockVecDot X (blockMatVecMul A X)

L-4. The quadratic form of a block whose flat representative is positive semidefinite is nonnegative. Used to discharge CH-3's hLsq side condition from its hE.

The quadratic half

theorem HCPolySupport.HighContrast.Multiscale.quadratic_le_norm_normalizedBlock {d : ℕ} (E H : BlockMat d) (hE : Matrix.PosDef (toFullBlockMat E)) (X : BlockVec d) : blockVecDot X (blockMatVecMul H X) ≤ ‖toFullBlockMat (normalizedBlock H E)‖ * blockVecDot X (blockMatVecMul E X)

The quadratic half. The unnormalized quadratic form of H is controlled by the operator norm of the E-NORMALIZED block times the E-quadratic form:

x · H x ≤ |E^{-1/2} H E^{-1/2}| (x · E x).

The same estimate is diagonalWeak_recent_response_quadratic_le, whose proof is the same three moves — congruence of the normalized block by E^{1/2} back to H, the change of variable y = E^{1/2} x, and the Loewner envelope of the normalized block. Two differences, both STRENGTHENINGS:

• the carrier blockSize D (blockIdentity d) is replaced by ‖toFullBlockMat D‖, which is what weakAverageDefect and CH-3's henergy print; and
• the earlier statement assumes IsSymmetricBlockMat E/H; here NEITHER symmetry of H nor a separate symmetry hypothesis on E is needed, because L-1 holds for arbitrary matrices and (toFullBlockMat E).PosDef already carries the symmetry of E.

The coarse energy map on the doubled response space

This module proves the coarse energy-map estimate on the doubled response space together with the intermediate steps it rests on. The estimate is reached by two chains: one reaches it through metricBlockNormSq_recent_difference_le and metricBlockNormSq_average_le_adaptedCellAtCenter, and the other through metricBlockNormSq_blockCellAverage_diagonalWeakState_le, which also applies metricBlockNormSq_average_le_adaptedCellAtCenter.

The chain is doubledResponseJ_zero_left → doubledResponseValue_le / doubledResponseValue_zero_left_eq → energy_map_le → energy_map_metric_le, and it is proved here in full.

The reflection order sits above this root: it supplies the comparison hypothesis hcmp of the metric estimate below, and the chain below does not depend on it. Only the single identity Sharp.blockVecDot_blockMatVecMul_blockScale is needed from that layer; the same identity already appears in ResponseTransferSkeleton.lean, and E-1 proves it again here so that this module's import edge stays at Loewner.

The final metric estimate is stated for an arbitrary reference block M : BlockMat d rather than the self-dual diagonal metric blockDiag m m⁻¹. That matrix plays no role in the proof — it occurs only as the left-hand side of the Loewner hypothesis and inside the conclusion's quadratic form — so taking M arbitrary is free, is strictly more general, and commits the estimate to no one metric encoding. Later layers may supply whichever of blockDiag m m⁻¹, blockSqrt (respM0 F) or normalizedBlock · · they print.

E-1 … E-2: flat helpers

E-3 … E-6: averages of a doubled field against a fixed load

E-7 … E-8: the doubled response at zero primal load

E-10 … E-11: the energy map

theorem HCPolySupport.HighContrast.Multiscale.energy_map_metric_le {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U a Y) (M : BlockMat d) {c : ℝ} (hc : 0 ≤ c) (hcmp : BlockMatLoewnerLE M (blockScale c (Book.Ch02.coarseStarredBlockMatrix U a))) : 1 / 2 * blockVecDot (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux) (blockMatVecMul M (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux)) ≤ c * (1 / 2 * Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (Y.eval x)))

E-11. The metric form of the energy map: once a reference block M is dominated by the starred coarse block, M ≤ c 𝐀_*(V) in the Loewner order, the M-size of the cell average is controlled by the cell energy, y·M y ≤ c ⨍_V Y·𝐀Y.

The estimate is stated for an arbitrary M : BlockMat d, in place of the self-dual diagonal metric blockDiag m m⁻¹; the generalisation is free because that matrix is never unfolded in the proof, and it keeps the result uncommitted to any one metric encoding.

This is the declaration both chains described in the header bottom out in.

theorem HCPolySupport.HighContrast.Multiscale.energy_map_congr_le {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U a Y) (R : BlockMat d) {c : ℝ} (hc : 0 ≤ c) (hcmp : BlockMatLoewnerLE (blockCongr R (Book.Ch02.blockIdentity d)) (blockScale c (Book.Ch02.coarseStarredBlockMatrix U a))) : blockVecDot (blockMatVecMul R (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux)) (blockMatVecMul R (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux)) ≤ c * Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (Y.eval x))

E-12 — the estimate in the form applied downstream. E-11 with the reference block taken to be a congruence R^T I R: a squared metric size |R (Y)_V|² of the cell average, with no factor ½ on either side.

This is the form the upper layers should use. It carries no symmetry hypothesis on R: blockVecDot_blockCongr already produces the congruence on the nose. The same shape is reached elsewhere by unfolding metricBlockNormSq at the end of metricBlockNormSq_average_le_adaptedCellAtCenter.