High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyCellRawMean

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

Raw comparison of a Whitney-cell mean with its initial chain ball

The first step of a convex Hardy chain compares the mean on a Whitney cell with the mean on its initial interior ball. The estimate retains the raw cross difference, as do the later links of the chain.

theorem HCPolySupport.HighContrast.convexHardyBallVolumeLower_le_volume_euclideanBallAt {d : ℕ} (hd : 1 ≤ d) (c : Vec d) {r : ℝ} (hr : 0 < r) : convexHardyBallVolumeLower d r ≤ MeasureTheory.volume (euclideanBallAt c r)

The explicit lower ball volume is bounded by the volume of every Euclidean ball of the corresponding radius.