High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.BallTerminalBranchEstimates

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

The two radius bands of the large-scale C¹ slope approximation's ball terminal

ExactRootGaugeTerminal asserts one decay estimate for every radius r ∈ Icc rStart R. The radius range necessarily splits at r = R / (108 √d):

• below the threshold (far branch) the canonical outer cube of r is at a generation q ≤ m, where m is the largest generation whose cube sits inside the ball of radius R, so the cube row applies and supplies the decay;
• above it (near band) 3 ^ q(r) overshoots 3 ^ m, the cube row is silent, and — because 2 ≤ d forces √d > 1 — the band is never empty: it always contains r = R.

This module renders both bands as standalone estimates over abstract data, so that the assembly only has to supply the geometry.

The near band consumes one hypothesis this module could not discharge, the weighted-energy triangle inequality on the closed ball (htri below). It is exactly Minkowski for ‖s^{1/2} ·‖_{L_underlined²(V)}; the repository has it only for H1Functions on triadic cubes (weightedGradNorm_sub_le_add_sub_h1), never for a general set. Its statement is passed in, never assumed globally.

noncomputable def HCPolySupport.HighContrast.CorrectorComposition.farBranchConstant (d : ℕ) : ℝ

The law-free geometric price of the far branch.

Equations

• HCPolySupport.HighContrast.CorrectorComposition.farBranchConstant d = ((6 * √↑d) ^ d) ^ (1 / 2) * (36 * √↑d) * ((12 * √↑d) ^ d) ^ (1 / 2)

noncomputable def HCPolySupport.HighContrast.CorrectorComposition.nearBranchConstant (d : ℕ) (B Aslope : ℝ) : ℝ

The law-free geometric price of the near band.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.CorrectorComposition.farBranchConstant_pos {d : ℕ} [NeZero d] : 0 < farBranchConstant d

A volume-ratio bound, lifted to the (1/2)-power

The far branch

theorem HCPolySupport.HighContrast.CorrectorComposition.farBranch_estimate (d : ℕ) [NeZero d] {aIdentity : Book.Ch03.CoeffFamily d} {bRef : CoeffField d} (hcoeff : ∀ (Q : TriadicCube d), bRef =ᵐ[MeasureTheory.volume] (aIdentity.coeffOn Q).toCoeffField) {eta A r R : ℝ} {q m : ℕ} (hetaNonneg : 0 ≤ eta) (hetaOne : eta ≤ 1) (hA : 0 < A) (hr : 0 < r) (hR : 0 < R) (hqm : q ≤ m) (hq3 : 3 ^ q ≤ 12 * r) (hcube : closedNormBall d r ⊆ openCubeSet (originCube d ↑q)) (hratioIn : MeasureTheory.volume (openCubeSet (originCube d ↑q)) / MeasureTheory.volume (closedNormBall d r) ≤ ENNReal.ofReal ((6 * √↑d) ^ d)) (hmR : √↑d * 3 ^ m ≤ R) (hmRmax : R < 3 * (√↑d * 3 ^ m)) (F G : Vec d → Vec d) (hrow : weightedGradNorm (aIdentity.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) F ≤ ENNReal.ofReal (A * Real.rpow 3 (-eta * ↑(m - q))) * weightedGradNorm (aIdentity.coeffOn (originCube d ↑m)).toCoeffField (openCubeSet (originCube d ↑m)) G) : weightedGradNorm bRef (closedNormBall d r) F ≤ ENNReal.ofReal (farBranchConstant d * A * (r / R) ^ eta) * weightedGradNorm bRef (closedNormBall d R) G

The far branch. Ball → canonical outer cube → cube row → inner cube → ball, with the generation gap converted to a radius ratio.

The near band

theorem HCPolySupport.HighContrast.CorrectorComposition.nearBranch_estimate (d : ℕ) [NeZero d] {aIdentity : Book.Ch03.CoeffFamily d} {bRef : CoeffField d} (hcoeff : ∀ (Q : TriadicCube d), bRef =ᵐ[MeasureTheory.volume] (aIdentity.coeffOn Q).toCoeffField) {eta B Aslope r R : ℝ} {m J : ℕ} {e : Vec d} (_hetaNonneg : 0 ≤ eta) (hetaOne : eta ≤ 1) (hB : 0 < B) (hAslope : 0 < Aslope) (hr : 0 < r) (hR : 0 < R) (hrR : r ≤ R) (hnear : R < 108 * (√↑d * r)) (hcubeJ : closedNormBall d R ⊆ openCubeSet (originCube d ↑J)) (hratioJ : MeasureTheory.volume (openCubeSet (originCube d ↑J)) / MeasureTheory.volume (closedNormBall d R) ≤ ENNReal.ofReal ((6 * √↑d) ^ d)) (hmR : √↑d * 3 ^ m ≤ R) (hmRmax : R < 3 * (√↑d * 3 ^ m)) (Du Cor : Vec d → Vec d) (htri : (weightedGradNorm bRef (closedNormBall d R) fun (y : Vec d) => Du y - Cor y) ≤ weightedGradNorm bRef (closedNormBall d R) Du + weightedGradNorm bRef (closedNormBall d R) Cor) (hcorEnergy : weightedGradNorm (aIdentity.coeffOn (originCube d ↑J)).toCoeffField (openCubeSet (originCube d ↑J)) Cor ≤ ENNReal.ofReal (B * euclideanNorm e)) (hslope : ENNReal.ofReal (euclideanNorm e) ≤ ENNReal.ofReal Aslope * weightedGradNorm (aIdentity.coeffOn (originCube d ↑m)).toCoeffField (openCubeSet (originCube d ↑m)) Du) : (weightedGradNorm bRef (closedNormBall d r) fun (y : Vec d) => Du y - Cor y) ≤ ENNReal.ofReal (nearBranchConstant d B Aslope * (r / R) ^ eta) * weightedGradNorm bRef (closedNormBall d R) Du

The near band. Ball → ball, then the triangle inequality, then the corrector's own energy against the solution's.