High-contrast homogenization: Provider.PolynomialHomogenization.ConvexFractionalInfiniteBallChain

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

Infinite dyadic ball chains in convex domains

noncomputable def HCPolySupport.HighContrast.convexFractionalChainScale (n : ℕ) : ℝ

Dyadic scale decreasing from one to zero.

Equations

• HCPolySupport.HighContrast.convexFractionalChainScale n = (1 / 2) ^ n

noncomputable def HCPolySupport.HighContrast.convexFractionalChainCenter {d : ℕ} (c x : Vec d) (n : ℕ) : Vec d

The center at level n on the segment from the sandwich center to x.

Equations

• HCPolySupport.HighContrast.convexFractionalChainCenter c x n = c + (1 - HCPolySupport.HighContrast.convexFractionalChainScale n) • (x - c)

def HCPolySupport.HighContrast.convexFractionalChainBall {d : ℕ} (c x : Vec d) (rho : ℝ) (n : ℕ) : Set (Vec d)

The level-n ball of the infinite segment chain.

Equations

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

theorem HCPolySupport.HighContrast.convexFractionalChainScale_pos (n : ℕ) : 0 < convexFractionalChainScale n

theorem HCPolySupport.HighContrast.convexFractionalChainScale_succ (n : ℕ) : convexFractionalChainScale (n + 1) = 1 / 2 * convexFractionalChainScale n

theorem HCPolySupport.HighContrast.convexFractionalChainBall_zero {d : ℕ} (c x : Vec d) (rho : ℝ) : convexFractionalChainBall c x rho 0 = euclideanBallAt c rho

theorem HCPolySupport.HighContrast.convexFractionalChainBall_subset {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {c x : Vec d} {rho : ℝ} (hrho : 0 < rho) (hinner : euclideanBallAt c rho ⊆ U) (hx : x ∈ U) (n : ℕ) : convexFractionalChainBall c x rho n ⊆ U

Every ball of the infinite segment chain lies in the convex domain.

theorem HCPolySupport.HighContrast.euclideanDist_convexFractionalChainCenter {d : ℕ} (c x : Vec d) (n : ℕ) : euclideanDist x (convexFractionalChainCenter c x n) = convexFractionalChainScale n * euclideanDist x c

The chain centers converge to the point x at the dyadic rate.

theorem HCPolySupport.HighContrast.euclideanDist_lt_scale_mul_add_of_mem_convexFractionalChainBall {d : ℕ} {U : Set (Vec d)} {c x y : Vec d} {rho Rad : ℝ} (houter : U ⊆ euclideanBallAt c Rad) (hx : x ∈ U) (hRad : 0 ≤ Rad) (hrho : 0 < rho) {n : ℕ} (hy : y ∈ convexFractionalChainBall c x rho n) : euclideanDist x y < convexFractionalChainScale n * (Rad + rho)

A member of the level-n ball is within the corresponding dyadic multiple of Rad + rho from the endpoint x.