High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyChainAtCenter #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Convex Hardy chains at a fixed sandwich center #
The ball-sandwich data provide one distinguished center. All chains used in the Whitney aggregation can be chosen with that same center while retaining the common scale bounds from the abstract chain construction.
theorem
HCPolySupport.HighContrast.exists_convexHardyBallChain_at_center_of_length
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{c : Vec d}
{rho Rad r : ℝ}
(hrho : 0 < rho)
(hRad : 0 ≤ Rad)
(hinner : euclideanBallAt c rho ⊆ U)
(houter : U ⊆ euclideanBallAt c Rad)
{x : Vec d}
(hx : x ∈ U)
(N : ℕ)
(hlower : r ≤ convexHardyBallChainRadius rho N 0)
(hupper : convexHardyBallChainRadius rho N 0 < 2 * r)
:
Prescribed initial-radius bounds construct a chain of exactly the given length at the distinguished sandwich center.