High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.OrderComparison

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

The finite-scale negative-order conversion and its cancellation

The first theorem is the exact duality conversion once the positive test-norm embedding is supplied. The remaining theorems certify the scale algebra that the inverse-radius statement consumes.

theorem HCPolySupport.HighContrast.negOneNorm_le_of_hsNormSq_le_h1NormSq {d : ℕ} {V : Set (Vec d)} {s K : ℝ} (hK : 0 < K) (hTest : ∀ (psi : Vec d → Vec d), IsLocalVecTest V psi → hsNormSq V s psi ≤ ENNReal.ofReal K * h1NormSq V psi) (F : Vec d → Vec d) : negOneNorm V F ≤ ENNReal.ofReal √K * negSobolevNorm V s F

A positive test-norm embedding gives the corresponding dual negative-order comparison without narrowing either test class.

theorem HCPolySupport.HighContrast.negOneNorm_pair_le_of_hsNormSq_le_h1NormSq {d : ℕ} {V : Set (Vec d)} {s K : ℝ} (hK : 0 < K) (hTest : ∀ (psi : Vec d → Vec d), IsLocalVecTest V psi → hsNormSq V s psi ≤ ENNReal.ofReal K * h1NormSq V psi) (F G : Vec d → Vec d) : negOneNorm V F + negOneNorm V G ≤ ENNReal.ofReal √K * (negSobolevNorm V s F + negSobolevNorm V s G)

The dual conversion applies jointly to the gradient and flux rows with one common positive embedding constant.

theorem HCPolySupport.HighContrast.inverse_scale_mul_order_loss (n : ℤ) (s : ℝ) : (3 ^ n)⁻¹ * 3 ^ ((1 - s) * ↑n) = 3 ^ (-s * ↑n)

Exact real exponent arithmetic behind the inverse-radius normalization.

theorem HCPolySupport.HighContrast.ofReal_inverse_scale_mul_order_loss (n : ℤ) (s : ℝ) : ENNReal.ofReal (3 ^ n)⁻¹ * ENNReal.ofReal (3 ^ ((1 - s) * ↑n)) = ENNReal.ofReal (3 ^ (-s * ↑n))

The same cancellation in the extended nonnegative carrier used by the frozen clause.

theorem HCPolySupport.HighContrast.printOrder_twoRow_feeds_v2_scale {d : ℕ} (n : ℤ) (s : ℝ) (A B : ENNReal) (F G : Vec d → Vec d) (hOrder : negOneNorm (openCubeSet (originCube d n)) F + negOneNorm (openCubeSet (originCube d n)) G ≤ A * ENNReal.ofReal (3 ^ ((1 - s) * ↑n)) * (negSobolevNorm (openCubeSet (originCube d n)) s F + negSobolevNorm (openCubeSet (originCube d n)) s G)) (hFractional : negSobolevNorm (openCubeSet (originCube d n)) s F + negSobolevNorm (openCubeSet (originCube d n)) s G ≤ B) : ENNReal.ofReal (3 ^ n)⁻¹ * negOneNorm (openCubeSet (originCube d n)) F + ENNReal.ofReal (3 ^ n)⁻¹ * negOneNorm (openCubeSet (originCube d n)) G ≤ A * ENNReal.ofReal (3 ^ (-s * ↑n)) * B

Consumer-side composition of the two-row fractional estimate, the finite-scale order comparison, and the inverse-radius normalization. The two analytic estimates remain explicit inputs; all scale accounting is proved here.