High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyCoreMean

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

Inverse-scale row mass in a convex Whitney system

The Whitney row-volume estimate and a geometric series control the total normalized inverse-scale mass of the cells. The retained factors support the fixed-cutoff aggregation of boundary and top rows.

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

The loss in comparing the mean on the common interior ball with the domain mean.

Equations

• HCPolySupport.HighContrast.convexHardyCoreMeanFactor d rho Rad s = 2 * (HCPolySupport.HighContrast.convexHardyBallVolumeLower d rho)⁻¹ * ENNReal.ofReal ((2 * Rad) ^ (↑d + 2 * s))

noncomputable def HCPolySupport.HighContrast.convexHardyCoreRowRatio (s : ℝ) : ENNReal

The ratio of the inverse-scale Whitney row series.

Equations

• HCPolySupport.HighContrast.convexHardyCoreRowRatio s = ENNReal.ofReal ((1 / 3) ^ (-2 * s)) * ENNReal.ofReal (1 / 3)

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

The normalized total inverse-scale volume bound for all Whitney rows up to the top scale n.

Equations

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