High-contrast homogenization: Setup.Geometry

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

Triadic and adapted geometry

The centered triadic cubes of s.introduction, the standard aligned cubes of e.coarse.ellipticity, the rounding convention of s.scale.selection, the adapted cells of a rounded geometry, and the ellipsoids of the homogenization theorem.

Triadic geometry

def HCPolySupport.HighContrast.centeredCube (d : ℕ) (m : ℤ) : Set (Vec d)

The centered open triadic cube □_m = (-3^m/2, 3^m/2)^d (the triadic cube of generation m).

Equations

• HCPolySupport.HighContrast.centeredCube d m = HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

def HCPolySupport.HighContrast.standardCell (d : ℕ) (k : ℤ) (w : Fin d → ℤ) : Set (Vec d)

The standard aligned cube z + □_k with z = 3^k w, w ∈ ℤ^d.

Equations

• HCPolySupport.HighContrast.standardCell d k w = HCPolySupport.openCubeSet (HCPolySupport.translateCube w (HCPolySupport.originCube d k))

noncomputable def HCPolySupport.HighContrast.standardCellCenter {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : Vec d

The center 3^k w of a standard aligned cube.

Equations

• HCPolySupport.HighContrast.standardCellCenter k w i = 3 ^ k * ↑(w i)

theorem HCPolySupport.HighContrast.standardCell_zero {d : ℕ} (k : ℤ) : standardCell d k 0 = centeredCube d k

The standard aligned cube at the zero index is the centered cube.

theorem HCPolySupport.HighContrast.standardCellCenter_zero_mem_centeredCube {d : ℕ} (k m : ℤ) : standardCellCenter k 0 ∈ centeredCube d m

The origin, the center of the standard cell at index zero, lies in every centered cube.

The rounding convention: k_0(d), rounded grids, adapted cells

def HCPolySupport.HighContrast.kZero (d : ℕ) : ℕ

The fixed rounding scale k_0(d) of the rounded adapted grid. Chosen concretely with slack; consumers use only kZero_spec.

Equations

• HCPolySupport.HighContrast.kZero d = d + 5

theorem HCPolySupport.HighContrast.kZero_spec (d : ℕ) : ↑d * 3 ^ (-↑(kZero d)) ≤ 1 / 101

The quantitative constraint the paper places on k_0(d): d 3^{-k_0(d)} ≤ 1/101.

noncomputable def HCPolySupport.HighContrast.roundedGrid {d : ℕ} (j : ℤ) (m : Mat d) : Mat d

The rounded grid Q_j(m) (the rounded adapted grid of a metric): (Q_j(m))_{ik} = 3^{-j} ⌈3^j |m^{-1}|^{1/2} (m^{1/2})_{ik}⌉.

Equations

• HCPolySupport.HighContrast.roundedGrid j m = Matrix.of fun (i k : Fin d) => 3 ^ (-j) * ↑⌈3 ^ j * √(HCPolySupport.HighContrast.specBound m⁻¹) * HCPolySupport.HighContrast.matSqrt m i k⌉

noncomputable def HCPolySupport.HighContrast.baseRoundedGrid {d : ℕ} (m : Mat d) : Mat d

The base rounded grid Q(m) := Q_{k_0(d)}(m).

Equations

• HCPolySupport.HighContrast.baseRoundedGrid m = HCPolySupport.HighContrast.roundedGrid (↑(HCPolySupport.HighContrast.kZero d)) m

def HCPolySupport.HighContrast.IsRoundedGrid {d : ℕ} (ℓ : ℤ) (q : Mat d) : Prop

A rounded adapted grid at alignment scale ℓ ≥ k_0(d): the rounding of a positive symmetric witness.

Equations

• HCPolySupport.HighContrast.IsRoundedGrid ℓ q = (↑(HCPolySupport.HighContrast.kZero d) ≤ ℓ ∧ ∃ (m : HCPolySupport.Mat d), Matrix.PosDef m ∧ q = HCPolySupport.HighContrast.roundedGrid ℓ m)

def HCPolySupport.HighContrast.adaptedCell {d : ℕ} (q : Mat d) (j : ℤ) : Set (Vec d)

The adapted cell ⋄_j^q = q □_j (the adapted cubes of a rounded geometry).

Equations

• HCPolySupport.HighContrast.adaptedCell q j = HCPolySupport.matVecMul q '' HCPolySupport.HighContrast.centeredCube d j

def HCPolySupport.HighContrast.adaptedLattice {d : ℕ} (q : Mat d) : Set (Vec d)

The adapted lattice 𝕃_q = q ℤ^d (the adapted cubes of a rounded geometry).

Equations

• HCPolySupport.HighContrast.adaptedLattice q = Set.range fun (w : Fin d → ℤ) => HCPolySupport.matVecMul q fun (i : Fin d) => ↑(w i)

def HCPolySupport.HighContrast.adaptedCellAt {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : Set (Vec d)

The aligned adapted cell z + ⋄_r^q with z = 3^r q w ∈ 3^r 𝕃_q.

Equations

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

def HCPolySupport.HighContrast.adaptedCellTranslate {d : ℕ} (q : Mat d) (j : ℤ) (y : Vec d) : Set (Vec d)

The translate y + ⋄_j^q of an adapted cell by an arbitrary vector.

Equations

• HCPolySupport.HighContrast.adaptedCellTranslate q j y = (fun (x : HCPolySupport.Vec d) => y + x) '' HCPolySupport.HighContrast.adaptedCell q j

Ellipsoids for the homogenization theorem

def HCPolySupport.HighContrast.ellipsoid {d : ℕ} (abar : Mat d) (r : ℝ) : Set (Vec d)

The ellipsoid E_r = {x : x · s_bar⁻¹ x ≤ λ_bar⁻¹ r²} of e.homogenized.ellipsoids, where s_bar = ½(ā + āᵗ) and λ_bar⁻¹ = |s_bar⁻¹|.

Equations

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