Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.ConvexHardyInitialMeanAggregation

High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyInitialMeanAggregation #

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

Initial-chain-mean aggregation on convex domains #

The initial ball mean is split at a common dyadic cutoff. The boundary-side part is supplied by the stopped chain, while the interior-side part is a single comparison with the domain mean.

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

The explicit coefficient for the initial-chain-mean comparison with the domain mean.

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