High-contrast homogenization: Provider.Quenched.SmallContrastRowCapIsotropy

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

The split primal row cap

The row is split at a scale 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 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.profilePrimalHattedEarlierRow_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.profilePrimalHattedEarlierRow P (roundedGrid l n) h0 s Pcen Qcen ≤ ENNReal.ofReal (2 * (1 + cIso) * (1 / (1 - 3 ^ (-(3 / 2)))) * Response.profileQuadraticLoad (Response.profileHattedBlock 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.profileHattedBlock h0 E) Pcen Qcen)

The split row cap (primal). 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.