High-contrast homogenization:

Provider.PolynomialHomogenization.ConvexFractionalChainBallVolumeScaling

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

Volume normalization for fractional convex chains

noncomputable def HCPolySupport.HighContrast.convexFractionalChainExactCoefficient {d : ℕ} (c x : Vec d) (rho Rad s : ℝ) (n : ℕ) : ENNReal

The exact-volume coefficient appearing in a chain jump.

Equations

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

noncomputable def HCPolySupport.HighContrast.convexFractionalChainLowerCoefficient (d : ℕ) (rho Rad s : ℝ) (n : ℕ) : ENNReal

The corresponding coefficient with both ball volumes replaced by the explicit dimension-dependent lower bounds.

Equations

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

theorem HCPolySupport.HighContrast.convexFractionalChainExactCoefficient_le_lowerCoefficient {d : ℕ} (hd : 1 ≤ d) (c x : Vec d) {rho Rad s : ℝ} (hrho : 0 < rho) (n : ℕ) : convexFractionalChainExactCoefficient c x rho Rad s n ≤ convexFractionalChainLowerCoefficient d rho Rad s n

Exact ball volumes are bounded by their explicit lower-volume normalization in the fractional chain coefficient.