High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.CubeToBallArithmetic

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

Cube-to-ball packaging: the decay conversion

The exact-gauge simultaneous-slope row decays in the triadic generation gap, 3 ^ (-η · (m - q)). The large-scale C¹ slope approximation clause terminal decays in the radius ratio, (r / R) ^ η. No declaration converts one to the other (the two existing generation-gap identities, HCPolySupport.HighContrast.Quenched.triadic_gap_rpow_eq and triadic_weight_inv_eq_gap_rpow, are private in HCPoly.Provider.Quenched.CoupledMixingScaleDecay, and both are single-endpoint).

This module supplies the conversion, order-generic and with an explicit law-free constant. It is the arithmetic half of the packaging; the geometric half is the sandwich

• ball r ⊆ openCubeSet (originCube d q) with 3 ^ q ≤ K₁ · r, and
• openCubeSet (originCube d m) ⊆ ball R with K₂ · R ≤ 3 ^ m,

for which the inclusions euclideanBall_subset_openCubeSet_originCube_outerTriadicGeneration and openCubeSet_originCube_subset_scaleMatchedEuclideanBall and the volume-ratio monotonicity weightedGradNorm_mono_set_le_volumeRatio are the ingredients.

theorem HCPolySupport.HighContrast.CorrectorComposition.triadicGap_rpow_eq {q m : ℕ} (hqm : q ≤ m) (eta : ℝ) : 3 ^ (-eta * ↑(m - q)) = (3 ^ q / 3 ^ m) ^ eta

The generation gap, rewritten as a scale ratio.

theorem HCPolySupport.HighContrast.CorrectorComposition.triadicGap_le_radiusRatio {q m : ℕ} (hqm : q ≤ m) {eta K₁ K₂ r R : ℝ} (heta : 0 ≤ eta) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hr : 0 < r) (hR : 0 < R) (hq : 3 ^ q ≤ K₁ * r) (hm : K₂ * R ≤ 3 ^ m) : 3 ^ (-eta * ↑(m - q)) ≤ (K₁ / K₂) ^ eta * (r / R) ^ eta

The decay conversion. A generation-gap decay becomes a radius-ratio decay, at the explicit law-free cost (K₁ / K₂) ^ η.