High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyBallChain

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

Ball chains in convex domains

A concentric ball sandwich supplies a canonical chain of interior balls from any point of the domain to the fixed inner ball. The centers lie on the segment from the point to the sandwich center, while the radii double at each step. The initial radius can be chosen between a prescribed positive scale and twice that scale.

The explicit indexing and center-distance bounds are designed for telescoping estimates between averages over successive balls.

noncomputable def HCPolySupport.HighContrast.convexHardyBallChainScale (N : ℕ) (i : Fin (N + 1)) : ℝ

The geometric scale at the i-th member of a chain of length N.

Equations

• HCPolySupport.HighContrast.convexHardyBallChainScale N i = 2 ^ ↑i / 2 ^ N

noncomputable def HCPolySupport.HighContrast.convexHardyBallChainCenter {d : ℕ} (c x : Vec d) (N : ℕ) (i : Fin (N + 1)) : Vec d

The center at the i-th member of the segment chain from x to c.

Equations

• HCPolySupport.HighContrast.convexHardyBallChainCenter c x N i = c + (1 - HCPolySupport.HighContrast.convexHardyBallChainScale N i) • (x - c)

noncomputable def HCPolySupport.HighContrast.convexHardyBallChainRadius (rho : ℝ) (N : ℕ) (i : Fin (N + 1)) : ℝ

The radius at the i-th member of a chain with terminal radius rho.

Equations

• HCPolySupport.HighContrast.convexHardyBallChainRadius rho N i = HCPolySupport.HighContrast.convexHardyBallChainScale N i * rho

structure HCPolySupport.HighContrast.ConvexHardyBallChain {d : ℕ} (U : Set (Vec d)) (x : Vec d) (rho Rad r : ℝ) : Type

Finite geometric ball-chain data at an initial scale r.

• center : Vec d

  Terminal center of the geometric ball chain.

• length : ℕ

  Number of successive radius doublings, giving a chain of one more ball.

• initial_radius_lower : r ≤ convexHardyBallChainRadius rho self.length 0
• initial_radius_upper : convexHardyBallChainRadius rho self.length 0 < 2 * r
• balls_subset (i : Fin (self.length + 1)) : euclideanBallAt (convexHardyBallChainCenter self.center x self.length i) (convexHardyBallChainRadius rho self.length i) ⊆ U
• terminal_center : convexHardyBallChainCenter self.center x self.length (Fin.last self.length) = self.center
• terminal_radius : convexHardyBallChainRadius rho self.length (Fin.last self.length) = rho
• radius_succ (i : Fin self.length) : convexHardyBallChainRadius rho self.length i.succ = 2 * convexHardyBallChainRadius rho self.length i.castSucc
• initial_center_dist : dist x (convexHardyBallChainCenter self.center x self.length 0) < Rad / rho * convexHardyBallChainRadius rho self.length 0
• center_dist_succ (i : Fin self.length) : dist (convexHardyBallChainCenter self.center x self.length i.castSucc) (convexHardyBallChainCenter self.center x self.length i.succ) < Rad / rho * convexHardyBallChainRadius rho self.length i.castSucc

theorem HCPolySupport.HighContrast.convexHardyBallChainScale_pos (N : ℕ) (i : Fin (N + 1)) : 0 < convexHardyBallChainScale N i

theorem HCPolySupport.HighContrast.convexHardyBallChainScale_le_one (N : ℕ) (i : Fin (N + 1)) : convexHardyBallChainScale N i ≤ 1

theorem HCPolySupport.HighContrast.convexHardyBallChainScale_zero (N : ℕ) : convexHardyBallChainScale N 0 = (1 / 2) ^ N

theorem HCPolySupport.HighContrast.convexHardyBallChainScale_last (N : ℕ) : convexHardyBallChainScale N (Fin.last N) = 1

theorem HCPolySupport.HighContrast.convexHardyBallChainScale_succ (N : ℕ) (i : Fin N) : convexHardyBallChainScale N i.succ = 2 * convexHardyBallChainScale N i.castSucc

theorem HCPolySupport.HighContrast.convexHardyBallChainCenter_last {d : ℕ} (c x : Vec d) (N : ℕ) : convexHardyBallChainCenter c x N (Fin.last N) = c

theorem HCPolySupport.HighContrast.convexHardyBallChainRadius_last (rho : ℝ) (N : ℕ) : convexHardyBallChainRadius rho N (Fin.last N) = rho

theorem HCPolySupport.HighContrast.convexHardyBallChainRadius_succ (rho : ℝ) (N : ℕ) (i : Fin N) : convexHardyBallChainRadius rho N i.succ = 2 * convexHardyBallChainRadius rho N i.castSucc

theorem HCPolySupport.HighContrast.euclideanBallAt_convexHardyBallChainCenter_subset {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c x : Vec d} {rho : ℝ} (hrho : 0 < rho) (hinner : euclideanBallAt c rho ⊆ U) (hx : x ∈ U) (N : ℕ) (i : Fin (N + 1)) : euclideanBallAt (convexHardyBallChainCenter c x N i) (convexHardyBallChainRadius rho N i) ⊆ U

Every member of the geometric chain is contained in the convex domain.

theorem HCPolySupport.HighContrast.dist_convexHardyBallChainCenter_succ {d : ℕ} (c x : Vec d) (N : ℕ) (i : Fin N) : dist (convexHardyBallChainCenter c x N i.castSucc) (convexHardyBallChainCenter c x N i.succ) = convexHardyBallChainScale N i.castSucc * dist x c

theorem HCPolySupport.HighContrast.dist_convexHardyBallChainCenter_zero {d : ℕ} (c x : Vec d) (N : ℕ) : dist x (convexHardyBallChainCenter c x N 0) = convexHardyBallChainScale N 0 * dist x c