High-contrast homogenization: Provider.Quenched.SmallContrastRowCapIsotropyAdjoint

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

The split adjoint row cap

This is the adjoint analogue of SmallContrastRowCapIsotropy, with profileHattedBlock replaced by profileHattedAdjointBlock throughout and the symmetry, positivity and quadratic transport routed through the adjoint sign congruence. The split, the two regions, and the constants are unchanged. The row is split at k₀:

• above the split the cells are charged to the isotropy comparison, at the constant envelope 1 + cIso. The raw row weight 3^{(3/2)(k-s)} is then summed on its own, at ratio 3^{-3/2} — no g is consumed, because the envelope no longer grows with depth;
• below the split the cells are charged to the coarse ellipticity envelope; g of the weight's 3/2 is consumed by the envelope's growth and the residual ratio is 3^{-(3/2-g)}, summable for every g < 3/2 and so on the whole frozen range. The deep leg carries the extra factor 3^{(3/2-g)((k₀-1)-s)}, which is the tiltGap-shaped discount: it can be made smaller than any prescribed tolerance by taking s - k₀ past a threshold logarithmic in boundaryConst·3^{gG}.

The per-cell argument is identical in the two regions and is factored out as row_term_le_adjoint at an abstract cell envelope.

The isotropy hypothesis is stated as the family it is used as; its producer is annealedBlock_adaptedCellAt_le_isotropy, which supplies exactly this shape uniformly in the aligned index.

The split row cap

theorem HCPolySupport.HighContrast.Quenched.profileAdjointHattedEarlierRow_le_isotropy_split {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (t : ℤ) {G : ℕ} (hDelta : 0 ≤ t + ↑G - 1 - sK) (hentry : sourceMomentTwo K ≤ 3 ^ (t + ↑G - sK)) {s : ℤ} (hst : s ≤ t) (hgeom : ∀ k ≤ s, ∀ w ∈ Response.alignedIndex (roundedGrid l n) k s, adaptedCellAt (roundedGrid l n) k w ⊆ centeredCube d (t + ↑G)) {k0 : ℤ} {cIso : ℝ} (hcIso : 0 ≤ cIso) (hiso : ∀ (k : ℤ), k0 ≤ k → k ≤ s → ∀ w ∈ Response.alignedIndex (roundedGrid l n) k s, BlockMatLoewnerLE (annealedBlock P (adaptedCellAt (roundedGrid l n) k w)) (blockScale (1 + cIso) E)) (h0 : Mat d) (Pcen Qcen : Vec d) : Response.profileAdjointHattedEarlierRow P (roundedGrid l n) h0 s Pcen Qcen ≤ ENNReal.ofReal (2 * (1 + cIso) * (1 / (1 - 3 ^ (-(3 / 2)))) * Response.profileQuadraticLoad (Response.profileHattedAdjointBlock h0 E) Pcen Qcen + 2 * (2 * boundaryConst Cd g n * 3 ^ (g * (↑(t + ↑G) - ↑s))) * (3 ^ ((3 / 2 - g) * (↑(k0 - 1) - ↑s)) * (1 / (1 - 3 ^ (-(3 / 2 - g))))) * Response.profileQuadraticLoad (Response.profileHattedAdjointBlock h0 E) Pcen Qcen)

The split row cap (adjoint). Above the split scale k₀ the cells are charged to the isotropy envelope 1 + cIso against the raw weight, at ratio 3^{-3/2}; below it they use the coarse ellipticity envelope at ratio 3^{-(3/2-g)}, and the deep leg carries the discount 3^{(3/2-g)((k₀-1)-s)}.

The first summand of the conclusion is Π-free. The second retains boundaryConst·3^{g((t+G)-s)}, multiplied by a factor that the gap s - k₀ drives below any prescribed tolerance.