High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyCutoffAggregation

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

Fixed-cutoff aggregation for convex Hardy chains

A common dyadic cutoff replaces the uniformly interior tail of every ball chain by one comparison with the domain mean. Short chains use their initial ball, so the construction has no exceptional row.

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

The explicit normalized cutoff-mean aggregation factor.

Equations

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

noncomputable def HCPolySupport.HighContrast.convexHardyPrefixGeometricFactor (beta : ℝ) : ENNReal

The infinite geometric-head factor used for the boundary-scale chain prefix.

Equations

• HCPolySupport.HighContrast.convexHardyPrefixGeometricFactor beta = (1 - ENNReal.ofReal (Real.rpow 2 (-beta)))⁻¹