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

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

EccentricityScaleDecay for the recent-difference energy map

This file proves the matrix-order, spectral and Minkowski-type facts the recent-difference energy map of the diagonal weak-norm estimate needs: the equivalence of a block's spectral bound with its operator norm at a positive semidefinite block, existence of a nonempty child-maximizer family, a Minkowski-type inequality for a normalized sum of block pairings, the Loewner comparison transported through a congruence, and the matrix-square-root identities that let it commute with the normalizer. The module serves the manuscript's p.response.transfer.

EccentricityScaleDecay part 2: matrix order, spectral carriers, Minkowski, head/tail

The matrix-order / spectral / Minkowski / head-tail package is in this file; the remaining declarations are in RecentHeadDefectHalves.lean; the target itself is in DiagonalWeakNormBound.lean.

Two declarations are public rather than private because their only consumers are in the next module: centered_metric_quadratic_le and nonempty_childMaximizerFamily. Everything else in this file stays private.

theorem HCPolySupport.HighContrast.Multiscale.blockSpecBound_eq_norm_of_posSemidef {d : ℕ} (N : BlockMat d) (hN : Matrix.PosSemidef (toFullBlockMat N)) : blockSpecBound N = ‖toFullBlockMat N‖

Quadratic comparison. On positive semidefinite blocks the spectral positive-part carrier blockSpecBound is exactly the full Euclidean operator norm.

theorem HCPolySupport.HighContrast.Multiscale.centered_metric_quadratic_le {d : ℕ} {M E D : FullBlockMat d} (hM : Matrix.PosDef M) (hE : Matrix.PosDef E) (x : FullBlockVec d) : Matrix.mulVec D x ⬝ᵥ M⁻¹.mulVec (Matrix.mulVec D x) ≤ ‖matSqrt M⁻¹ * E * matSqrt M⁻¹‖ * ‖matSqrt E⁻¹ * D * matSqrt E⁻¹‖ ^ 2 * x ⬝ᵥ Matrix.mulVec E x

Quadratic comparison. A centered defect measured in M⁻¹ is controlled by the M-relative size of E, the E-normalized defect norm, and the E-quadratic load.

theorem HCPolySupport.HighContrast.Multiscale.nonempty_childMaximizerFamily {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (F : BlockMat d) (a : CoeffSpace d) (p r : Vec d) : Nonempty ((n : ℕ) → (w : Fin d → ℤ) → ScalarCanonicalMaximizer (adaptedCellAtCenter q (t - ↑n) w) p r (respCoeffMinus F a))

Parent/child decomposition. Child response maximizers can be chosen simultaneously at every depth and cell label.

theorem HCPolySupport.HighContrast.Multiscale.normalized_blockL2_add_le {d : ℕ} {iota : Type u_1} (Z : Finset iota) (u v : iota → BlockVec d) : √((↑Z.card)⁻¹ * ∑ z ∈ Z, blockVecDot (u z + v z) (u z + v z)) ≤ √((↑Z.card)⁻¹ * ∑ z ∈ Z, blockVecDot (u z) (u z)) + √((↑Z.card)⁻¹ * ∑ z ∈ Z, blockVecDot (v z) (v z))

Parent/child decomposition. The normalized finite-cell L² length obeys Minkowski's inequality for doubled vectors.

Helper lemmas. The LEFT-hand side of the target is not literally a

cellAverageFamily: it is the family of M_0^{1/2}-transported, U_t-recentred cell averages. The Jensen and summability lemmas are stated for a bare cellAverageFamily, so none applies to the goal. The transport and recentring helpers close that gap (they commute with the cell average, given integrability), and the window-split helpers supply the split at H that the printed right-hand side has: a finite head weighted exactly as weakCellSum is, plus a geometric tail whose weight is dominated by the printed 3^{-alpha H}.