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

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

The head's averaged-energy hypothesis at the estimate's carriers

The finite-window head of the diagonal weak-norm estimate needs, at each depth, the flat average over the triadic index box of twice the scalar difference energy between the parent and child response maximizers, bounded by the response load times the operator norm of the averaged normalized block defect. The recentred coefficient is only an almost-everywhere class and is never elliptic pointwise, so this file runs the identity at an almost-everywhere-equal elliptic representative, transporting the maximizers to it and the resulting bound back, leaving no pointwise ellipticity or coefficient-dependent integrability hypothesis in the conclusion. It supplies the averaged-energy hypothesis consumed by the cell-average estimate of the weak-norm bound e.response.weak.estimate.

The averaged-energy hypothesis of the cell-average estimate at the estimate's carriers

The cell-average estimate of the weak-norm bound (e.response.weak.estimate) consumes, at each depth n, a per-cell family whose flat average over the triadic index box is bounded by the printed product of the response load and the operator norm of the averaged normalized block defect. The per-cell half of that estimate produces G w as twice the scalar difference energy of the maximizers u and v w on the aligned subcell adaptedCellAtCenter (respGrid jStar F) (t - n) w:

G w = 2 ⨍_{V w} (∇u − ∇v_w) · symmPart(a_-) (∇u − ∇v_w).

The response identity that turns the flat average of those difference energies into the averaged response deficit is stated for a coefficient that is pointwise elliptic on the cell. The recentred coefficient a_- = respCoeffMinus F a is only an almost-everywhere class and is never elliptic pointwise, so the identity cannot be instantiated at it directly. This module runs the identity at an almost-everywhere-equal elliptic representative of a_-, transports the maximizers to that representative, and transports the conclusion back: every quantity in the conclusion is almost-everywhere invariant in the coefficient. The result therefore carries none of the pointwise ellipticity or coefficient-dependent integrability hypotheses that the representative argument removes.

The algebraic tail is the printed chain: the pointwise identity optimizerField b u − optimizerField b v = (∇u − ∇v, b (∇u − ∇v)) turns the doubled optimizer difference energy into the symmetric scalar difference energy, the recombined quadratic-response identity rewrites the flat average of the difference energies as twice the deficit of the response functional, each response value is the coarse-block quadratic form of its cell, and the averaged response deficit is the quadratic form of the averaged block defect, bounded by the normalized Loewner comparison through the response load and the operator norm of the averaged normalized defect. See e.response.weak.estimate.

theorem HCPolySupport.HighContrast.Multiscale.headEnergy_carrier_minus {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) (hgrid : IsUnit (respGrid jStar F)) (a : CoeffSpace d) (n : ℕ) (u : AHarmonicFunction (respCoeffMinus F a) (respCell jStar F t)) (hu : IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a) u) (v : (w : Fin d → ℤ) → AHarmonicFunction (respCoeffMinus F a) (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) w)) (hv : ∀ w ∈ triadicIndexBox d n, IsResponseMaximizer (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) w) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a) (v w)) (hEhat : Matrix.PosDef (toFullBlockMat (respEhatMinus P jStar F t))) : ((↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, 2 * volumeAverage (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) w) fun (x : Vec d) => vecDot (optimizerField (respCoeffMinus F a) u x - optimizerField (respCoeffMinus F a) (v w) x).1 (optimizerField (respCoeffMinus F a) u x - optimizerField (respCoeffMinus F a) (v w) x).2) ≤ 2 * respLsqMinus P jStar F t e * ‖toFullBlockMat (weakAverageDefect (respGrid jStar F) t n (respEhatMinus P jStar F t) (respCoeffMinus F a))‖

The averaged-energy hypothesis of the cell-average estimate, with no pointwise ellipticity hypothesis. For the per-cell family that is twice the scalar difference energy of the maximizers u and v w on the aligned subcells adaptedCellAtCenter (respGrid jStar F) (t - n) w, the flat average over the triadic index box is bounded by twice the response load times the operator norm of the averaged normalized block defect weakAverageDefect.

The identity is run at an almost-everywhere-equal representative f of respCoeffMinus F a that is pointwise elliptic on the parent adapted cell; the parent and child maximizers are transported to f along the almost-everywhere equality, and the resulting identity is transported back because both the scalar difference energy and each response value depend on the coefficient only through its almost-everywhere class. No pointwise ellipticity and no coefficient-dependent integrability hypothesis remains. See e.response.weak.estimate.