High-contrast homogenization: Provider.Quenched.SmallContrastCenteringCap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The centering cap #
The two centering pairings of the one-step hub, at the calibrated loads of
the response metric, are second order in the hatted contrast defect: the
closed Schur forms of the pairing identities are estimated by the generic
centering estimate, whose smallness clauses are supplied by the hatted
contrast of the annealed block alone. The cap constant is 3d + 4, half
the generic constant.
theorem
HCPolySupport.HighContrast.Quenched.centering_pairing_caps
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(U : Book.Ch02.Domain d)
(hint : HasIntegrableCoarseBlock P U.carrier)
{S SStar K : Mat d}
(hS : Matrix.PosDef S)
(hStar : Matrix.PosDef SStar)
(hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K)
{eps : ℝ}
(hpos : 0 < eps)
(heps1 : eps ≤ 1)
(htr : ↑d * (schurHattedContrast S SStar - 1) ≤ eps)
(e : Vec d)
(he : e ⬝ᵥ e = 1)
:
1 / 2 * |vecDot
(fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew (Response.responseSkew K) ⋯).coeffOn U)
(Response.centeredResponseOptimizer U (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P)
fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew (Response.responseSkew K) ⋯).coeffOn U)
(Response.centeredResponseOptimizer U (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P| ≤ (3 * ↑d + 4) * eps ^ 2 ∧ 1 / 2 * |vecDot
(fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew (Response.responseSkew K) ⋯).transpose.coeffOn U)
(Response.centeredAdjointOptimizer U (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P)
fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew (Response.responseSkew K) ⋯).transpose.coeffOn U)
(Response.centeredAdjointOptimizer U (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P| ≤ (3 * ↑d + 4) * eps ^ 2
The centering cap. Both centering pairings at the calibrated loads
are bounded by (3d + 4)·ε² whenever d·(hat − 1) ≤ ε ≤ 1.
theorem
HCPolySupport.HighContrast.Quenched.centering_caps_at_terminal
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(hfin : HasFiniteAdaptedMean P q t)
{S SStar K : Mat d}
(hS : Matrix.PosDef S)
(hStar : Matrix.PosDef SStar)
(hform : toFullBlockMat (adaptedMean P q t) = schurBlock S SStar K)
{eps : ℝ}
(hpos : 0 < eps)
(heps1 : eps ≤ 1)
(htr : ↑d * (schurHattedContrast S SStar - 1) ≤ eps)
(e : Vec d)
(he : e ⬝ᵥ e = 1)
:
1 / 2 * |vecDot
(fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageGradient (Response.adaptedDomain hq t)
((a.subSkew (Response.responseSkew K) ⋯).coeffOn (Response.adaptedDomain hq t))
(Response.centeredResponseOptimizer (Response.adaptedDomain hq t)
(a.subSkew (Response.responseSkew K) ⋯) (Response.centeredResponseLoadP S SStar K e)
(Response.centeredResponseLoadQ S SStar K e))
i ∂P)
fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageFlux (Response.adaptedDomain hq t)
((a.subSkew (Response.responseSkew K) ⋯).coeffOn (Response.adaptedDomain hq t))
(Response.centeredResponseOptimizer (Response.adaptedDomain hq t) (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P| ≤ (3 * ↑d + 4) * eps ^ 2 ∧ 1 / 2 * |vecDot
(fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageGradient (Response.adaptedDomain hq t)
((a.subSkew (Response.responseSkew K) ⋯).transpose.coeffOn (Response.adaptedDomain hq t))
(Response.centeredAdjointOptimizer (Response.adaptedDomain hq t) (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P)
fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageFlux (Response.adaptedDomain hq t)
((a.subSkew (Response.responseSkew K) ⋯).transpose.coeffOn (Response.adaptedDomain hq t))
(Response.centeredAdjointOptimizer (Response.adaptedDomain hq t) (a.subSkew (Response.responseSkew K) ⋯)
(Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e))
i ∂P| ≤ (3 * ↑d + 4) * eps ^ 2
The centering cap at the terminal adapted cell: the instance of the
cap at U := adaptedDomain hq t, phrased on the adapted mean — exactly the
two centering clauses of the one-step hub's hcaps hypothesis, at
Z := (3d + 4)·ε².