High-contrast homogenization: Entry.Geometry.AdaptedCell

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

Adapted cells

The adapted cell ⋄_j^q = q □_j and its translate W = y + ⋄_j^q of the paper, together with the two facts about W that l.source.whitney uses: its volume under the change of variables x = y + q v, and the strip estimate |{x ∈ W : dist(x, ∂W) ≤ s}| / |W| ≤ 2 d |q⁻¹| s 3^{-j}.

The definitions adaptedCell and adaptedCellTranslate live in HCPoly.Setup.Geometry (imported here), so that they can be used without these proofs. The bound |q⁻¹| ≤ K of e.rounded.grid.bounds enters only through the hypothesis InverseNormLE q K, i.e. |v| ≤ K |q v| for all v (stated with squared Euclidean norms).

Definitions

def HCPolySupport.HighContrast.Geometry.InverseNormLE {d : ℕ} (q : Mat d) (K : ℝ) : Prop

The operator-norm bound |q⁻¹| ≤ K, in the form |v|² ≤ K² |q v|² for every v.

Equations

• HCPolySupport.HighContrast.Geometry.InverseNormLE q K = ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq v ≤ K ^ 2 * HCPolySupport.vecNormSq (HCPolySupport.matVecMul q v)

theorem HCPolySupport.HighContrast.Geometry.matVecMul_eq_mulVec {d : ℕ} (q : Mat d) (v : Vec d) : matVecMul q v = Matrix.mulVec q v

theorem HCPolySupport.HighContrast.Geometry.mem_adaptedCellTranslate_iff {d : ℕ} {q : Mat d} {j : ℤ} {y x : Vec d} : x ∈ adaptedCellTranslate q j y ↔ ∃ v ∈ centeredCube d j, y + matVecMul q v = x

Volume under the change of variables

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCellTranslate {d : ℕ} (q : Mat d) (j : ℤ) (y : Vec d) : MeasureTheory.volume (adaptedCellTranslate q j y) = ENNReal.ofReal |Matrix.det q| * ENNReal.ofReal (3 ^ j) ^ d

Invertibility from the inverse bound

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_eq_zero_iff {d : ℕ} {v : Vec d} : vecNormSq v = 0 ↔ v = 0

theorem HCPolySupport.HighContrast.Geometry.InverseNormLE.isUnit {d : ℕ} {q : Mat d} {K : ℝ} (hq : InverseNormLE q K) : IsUnit q

theorem HCPolySupport.HighContrast.Geometry.InverseNormLE.det_ne_zero {d : ℕ} {q : Mat d} {K : ℝ} (hq : InverseNormLE q K) : Matrix.det q ≠ 0

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCellTranslate_pos {d : ℕ} {q : Mat d} {K : ℝ} (hq : InverseNormLE q K) (j : ℤ) (y : Vec d) : 0 < MeasureTheory.volume (adaptedCellTranslate q j y)

theorem HCPolySupport.HighContrast.Geometry.adaptedCellTranslate_eq_preimage {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) (y : Vec d) : adaptedCellTranslate q j y = (fun (x : Fin d → ℝ) => q⁻¹.mulVec (x - y)) ⁻¹' centeredCube d j

For invertible q, the translate y + q □_j is the preimage of □_j under x ↦ q⁻¹ (x - y).

theorem HCPolySupport.HighContrast.Geometry.isOpen_adaptedCellTranslate {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) (y : Vec d) : IsOpen (adaptedCellTranslate q j y)

The strip estimate

def HCPolySupport.HighContrast.Geometry.boundaryStrips (d : ℕ) (j : ℤ) (t : ℝ) : Set (Vec d)

The part of □_j within t of its boundary, coordinatewise: points of □_j with some coordinate of absolute value at least 3^j/2 - t.

Equations

• HCPolySupport.HighContrast.Geometry.boundaryStrips d j t = {v : HCPolySupport.Vec d | v ∈ HCPolySupport.HighContrast.centeredCube d j ∧ ∃ (i : Fin d), 1 / 2 * 3 ^ j - t ≤ |v i|}

def HCPolySupport.HighContrast.Geometry.coordStrip (d : ℕ) (j : ℤ) (t : ℝ) (i : Fin d) : Set (Vec d)

One coordinate strip of □_j of width t, as a product set.

Equations

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

theorem HCPolySupport.HighContrast.Geometry.volume_boundaryStrips_le {d : ℕ} (j : ℤ) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.volume (boundaryStrips d j t) ≤ ENNReal.ofReal (2 * ↑d * t * (3 ^ j) ^ (d - 1))

theorem HCPolySupport.HighContrast.Geometry.mem_image_boundaryStrips {d : ℕ} {q : Mat d} {K : ℝ} (hK : 0 ≤ K) (hq : InverseNormLE q K) {j : ℤ} {y x x' : Vec d} {s : ℝ} (hs : 0 ≤ s) (hx : x ∈ adaptedCellTranslate q j y) (hx' : x' ∉ adaptedCellTranslate q j y) (hdist : ∑ i : Fin d, (x i - x' i) ^ 2 ≤ s ^ 2) : x ∈ (fun (v : Vec d) => y + matVecMul q v) '' boundaryStrips d j (K * s)

Points of W within Euclidean distance s of a point outside W lie in the image of the boundary strips of width K s.

theorem HCPolySupport.HighContrast.Geometry.volume_le_of_near_complement {d : ℕ} [NeZero d] {q : Mat d} {K : ℝ} (hK : 0 ≤ K) (hq : InverseNormLE q K) {j : ℤ} {y : Vec d} {A : Set (Vec d)} {s : ℝ} (hs : 0 ≤ s) (hAW : A ⊆ adaptedCellTranslate q j y) (hA : ∀ x ∈ A, ∃ x' ∉ adaptedCellTranslate q j y, ∑ i : Fin d, (x i - x' i) ^ 2 ≤ s ^ 2) : MeasureTheory.volume A ≤ ENNReal.ofReal (2 * ↑d * (K * s) * 3 ^ (-j)) * MeasureTheory.volume (adaptedCellTranslate q j y)

The strip estimate. If every point of A ⊆ W is within Euclidean distance s of a point outside W, then |A| ≤ 2 d K s 3^{-j} |W|, where |q⁻¹| ≤ K.