High-contrast homogenization: Entry.Geometry.RoundedGridBasic

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

Rounded Grid Basic

The rounded grid 𝒬(𝔪) and its elementary properties. For a positive matrix 𝔪 and 3^{j_*} ≥ 2d, the entrywise definition (𝒬(𝔪))_{ab} = 3^{-j_*} ⌈3^{j_*} |𝔪⁻¹|^{1/2} (𝔪^{1/2})_{ab}⌉ gives a symmetric matrix whose rounding error from |𝔪⁻¹|^{1/2} 𝔪^{1/2} has operator norm at most d 3^{-j_*} ≤ 1/2, and the three estimates of e.rounded.grid.bounds hold — 𝒬(𝔪) ≥ ½ Id, |𝒬(𝔪)⁻¹| ≤ 2 and |𝒬(𝔪)| ≤ 2 (|𝔪| |𝔪⁻¹|)^{1/2} — together with 3^j 𝒬(𝔪) ℤ^d ⊆ ℤ^d for j ≥ j_*. The module also derives l.source.whitney for the source-shaped cells defined by 𝒬(𝔪) and records the comparison with the Euclidean grid used by the initialization.

The rounded grid 𝒬(𝔪) — definition only

Near e.rounded.grid.bounds. Fix j_* ∈ ℕ. For every matrix 𝔪,

(𝒬(𝔪))_{ab} := 3^{-j_*} ⌈ 3^{j_*} |𝔪⁻¹|^{1/2} (𝔪^{1/2})_{ab} ⌉.

Here |·| is the Euclidean operator norm (Mathlib's ‖·‖ under Matrix.Norms.L2Operator) and 𝔪^{1/2} is CFC.sqrt 𝔪. j_* is a parameter of the definition (the entries depend on it); the standing constraint 3^{j_*} ≥ 2d is a hypothesis on the theorems that use it.

This module is a definition-only leaf: it holds explicitRoundedGrid and nothing else. Every theorem about explicitRoundedGrid, including e.rounded.grid.bounds, lives in HCPoly.Entry.Geometry.RoundedGrid, which imports this module.

noncomputable def HCPolySupport.HighContrast.Geometry.explicitRoundedGrid {d : ℕ} (jStar : ℕ) (m : Mat d) : Mat d

The rounded grid 𝒬(𝔪), entrywise as printed: (𝒬(𝔪))_{ab} = 3^{-j_*} ⌈ 3^{j_*} |𝔪⁻¹|^{1/2} (𝔪^{1/2})_{ab} ⌉.

This is not the roundedGrid of HCPolySupport.HighContrast (HCPoly/Setup/Geometry.lean), which takes the scale as an integer and writes the same entries through specBound (the scalar Loewner bound) and matSqrt (the chosen positive-semidefinite square root). Here the scale is the natural number j_* and the entries are written out with the Euclidean operator norm and CFC.sqrt, so the two agree on positive definite arguments at integer scales but not by unfolding.

Equations

• HCPolySupport.HighContrast.Geometry.explicitRoundedGrid jStar m = Matrix.of fun (a b : Fin d) => 3 ^ (-↑jStar) * ↑⌈3 ^ jStar * √‖m⁻¹‖ * CFC.sqrt m a b⌉

The rounded grid 𝒬(𝔪) and e.rounded.grid.bounds

Near e.rounded.grid.bounds. Fix j_* ∈ ℕ with 3^{j_*} ≥ 2d. For every positive matrix 𝔪,

(𝒬(𝔪))_{ab} := 3^{-j_*} ⌈ 3^{j_*} |𝔪⁻¹|^{1/2} (𝔪^{1/2})_{ab} ⌉.

Here |·| is the Euclidean operator norm (Mathlib's ‖·‖ under Matrix.Norms.L2Operator) and 𝔪^{1/2} is CFC.sqrt 𝔪. The print asserts: 𝒬(𝔪) is symmetric; the rounding error has operator norm at most d 3^{-j_*} ≤ 1/2; the unrounded matrix |𝔪⁻¹|^{1/2} 𝔪^{1/2} has smallest eigenvalue 1 and largest eigenvalue (|𝔪| |𝔪⁻¹|)^{1/2}; hence (e.rounded.grid.bounds)

q ≥ ½ Id, |q⁻¹| ≤ 2, |q| ≤ 2 (|𝔪| |𝔪⁻¹|)^{1/2} for q = 𝒬(𝔪);

and 3^j q ℤ^d ⊆ ℤ^d for j ≥ j_*.

The definition explicitRoundedGrid itself lives in the definition-only leaf HCPoly.Entry.Geometry.RoundedGridDef (imported here), separately from the proofs below. j_* is a parameter of the definition (the entries depend on it) and the standing constraint 3^{j_*} ≥ 2d is a hypothesis hj on the theorems that use it; symmetry and the entrywise rounding bound do not need it. Each of the three bounds is given in the vector form used by l.source.whitney and in Mathlib's operator-norm (or Loewner-order) form. The bridge to node 1 is inverseNormLE_roundedGrid, and source_whitney_roundedGrid is the printed lemma with q = 𝒬(𝔪).

Definitions

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

The unrounded matrix |𝔪⁻¹|^{1/2} 𝔪^{1/2}.

Equations

• HCPolySupport.HighContrast.Geometry.unroundedGrid m = √‖m⁻¹‖ • CFC.sqrt m

theorem HCPolySupport.HighContrast.Geometry.unroundedGrid_apply {d : ℕ} (m : Mat d) (a b : Fin d) : unroundedGrid m a b = √‖m⁻¹‖ * CFC.sqrt m a b

theorem HCPolySupport.HighContrast.Geometry.explicitRoundedGrid_apply {d : ℕ} (jStar : ℕ) (m : Mat d) (a b : Fin d) : explicitRoundedGrid jStar m a b = (3 ^ jStar)⁻¹ * ↑⌈3 ^ jStar * unroundedGrid m a b⌉

Symmetry

theorem HCPolySupport.HighContrast.Geometry.explicitRoundedGrid_transpose {d jStar : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : Matrix.transpose (explicitRoundedGrid jStar m) = explicitRoundedGrid jStar m

The rounding error

theorem HCPolySupport.HighContrast.Geometry.abs_roundedGrid_sub_unroundedGrid_le {d : ℕ} (jStar : ℕ) (m : Mat d) (a b : Fin d) : |explicitRoundedGrid jStar m a b - unroundedGrid m a b| ≤ (3 ^ jStar)⁻¹

Each entry of the rounding error ⌈x⌉ - x scaled by 3^{-j_*} has absolute value at most 3^{-j_*}.

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_roundingError_mulVec_le {d : ℕ} (jStar : ℕ) (m : Mat d) (v : Vec d) : vecNormSq (Matrix.mulVec (explicitRoundedGrid jStar m - unroundedGrid m) v) ≤ (↑d * (3 ^ jStar)⁻¹) ^ 2 * vecNormSq v

The rounding error has operator norm at most d 3^{-j_*}, in vector form.

theorem HCPolySupport.HighContrast.Geometry.opNorm_roundingError_le {d : ℕ} (jStar : ℕ) (m : Mat d) : ‖explicitRoundedGrid jStar m - unroundedGrid m‖ ≤ ↑d * (3 ^ jStar)⁻¹

The rounding error has operator norm at most d 3^{-j_*}.

theorem HCPolySupport.HighContrast.Geometry.mul_inv_pow_le_half {d jStar : ℕ} (hj : 2 * d ≤ 3 ^ jStar) : ↑d * (3 ^ jStar)⁻¹ ≤ 1 / 2

The standing 3^{j_*} ≥ 2d gives d 3^{-j_*} ≤ 1/2.

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_roundingError_mulVec_le_half {d jStar : ℕ} (m : Mat d) (hj : 2 * d ≤ 3 ^ jStar) (v : Vec d) : vecNormSq (Matrix.mulVec (explicitRoundedGrid jStar m - unroundedGrid m) v) ≤ (1 / 2) ^ 2 * vecNormSq v

The rounding error has operator norm at most 1/2, in vector form.

theorem HCPolySupport.HighContrast.Geometry.abs_dotProduct_roundingError_le {d jStar : ℕ} (m : Mat d) (hj : 2 * d ≤ 3 ^ jStar) (v : Vec d) : |v ⬝ᵥ Matrix.mulVec (explicitRoundedGrid jStar m - unroundedGrid m) v| ≤ 1 / 2 * vecNormSq v

The unrounded matrix

theorem HCPolySupport.HighContrast.Geometry.dotProduct_unroundedGrid {d : ℕ} (m : Mat d) (v : Vec d) : v ⬝ᵥ Matrix.mulVec (unroundedGrid m) v = √‖m⁻¹‖ * v ⬝ᵥ (CFC.sqrt m).mulVec v

theorem HCPolySupport.HighContrast.Geometry.dotProduct_roundedGrid_eq {d : ℕ} (jStar : ℕ) (m : Mat d) (v : Vec d) : v ⬝ᵥ Matrix.mulVec (explicitRoundedGrid jStar m) v = v ⬝ᵥ Matrix.mulVec (unroundedGrid m) v + v ⬝ᵥ Matrix.mulVec (explicitRoundedGrid jStar m - unroundedGrid m) v

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_le_dotProduct_unroundedGrid {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (v : Vec d) : vecNormSq v ≤ v ⬝ᵥ Matrix.mulVec (unroundedGrid m) v

The smallest eigenvalue of the unrounded matrix is at least one: |v|² ≤ ⟨v, U v⟩.

theorem HCPolySupport.HighContrast.Geometry.dotProduct_unroundedGrid_le {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (v : Vec d) : v ⬝ᵥ Matrix.mulVec (unroundedGrid m) v ≤ √(‖m‖ * ‖m⁻¹‖) * vecNormSq v

The largest eigenvalue of the unrounded matrix is at most (|𝔪| |𝔪⁻¹|)^{1/2}: ⟨v, U v⟩ ≤ (‖𝔪‖ ‖𝔪⁻¹‖)^{1/2} |v|².

e.rounded.grid.bounds, first bound: q ≥ ½ Id

theorem HCPolySupport.HighContrast.Geometry.half_vecNormSq_le_dotProduct_roundedGrid {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (v : Vec d) : 1 / 2 * vecNormSq v ≤ v ⬝ᵥ Matrix.mulVec (explicitRoundedGrid jStar m) v

theorem HCPolySupport.HighContrast.Geometry.dotProduct_roundedGrid_nonneg {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (v : Vec d) : 0 ≤ v ⬝ᵥ Matrix.mulVec (explicitRoundedGrid jStar m) v

Second bound: |q⁻¹| ≤ 2, and the bridge to l.source.whitney

theorem HCPolySupport.HighContrast.Geometry.inverseNormLE_roundedGrid {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) : InverseNormLE (explicitRoundedGrid jStar m) 2

The bridge to node 1: q = 𝒬(𝔪) satisfies |v|² ≤ 4 |q v|², i.e. |q⁻¹| ≤ 2.

theorem HCPolySupport.HighContrast.Geometry.isUnit_roundedGrid {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) : IsUnit (explicitRoundedGrid jStar m)

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_roundedGrid_inv_mulVec_le {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (w : Vec d) : vecNormSq ((explicitRoundedGrid jStar m)⁻¹.mulVec w) ≤ 2 ^ 2 * vecNormSq w

|q⁻¹| ≤ 2 in vector form: |q⁻¹ w|² ≤ 2² |w|².

theorem HCPolySupport.HighContrast.Geometry.opNorm_roundedGrid_inv_le {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) : ‖(explicitRoundedGrid jStar m)⁻¹‖ ≤ 2

|q⁻¹| ≤ 2 for the Euclidean operator norm.

Third bound: |q| ≤ 2 (|𝔪| |𝔪⁻¹|)^{1/2}

theorem HCPolySupport.HighContrast.Geometry.one_le_opNorm_mul_opNorm_inv {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) {v : Vec d} (hv : v ≠ 0) : 1 ≤ ‖m‖ * ‖m⁻¹‖

|𝔪| |𝔪⁻¹| ≥ 1 as soon as there is a nonzero vector.

theorem HCPolySupport.HighContrast.Geometry.dotProduct_roundedGrid_le {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (v : Vec d) : v ⬝ᵥ Matrix.mulVec (explicitRoundedGrid jStar m) v ≤ 2 * √(‖m‖ * ‖m⁻¹‖) * vecNormSq v

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_roundedGrid_mulVec_le {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (v : Vec d) : vecNormSq (Matrix.mulVec (explicitRoundedGrid jStar m) v) ≤ (2 * √(‖m‖ * ‖m⁻¹‖)) ^ 2 * vecNormSq v

|q| ≤ 2 (|𝔪| |𝔪⁻¹|)^{1/2} in vector form.

theorem HCPolySupport.HighContrast.Geometry.opNorm_roundedGrid_le {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) : ‖explicitRoundedGrid jStar m‖ ≤ 2 * √(‖m‖ * ‖m⁻¹‖)

|q| ≤ 2 (|𝔪| |𝔪⁻¹|)^{1/2} for the Euclidean operator norm.

Integrality: 3^j 𝒬(𝔪) ℤ^d ⊆ ℤ^d for j ≥ j_*

theorem HCPolySupport.HighContrast.Geometry.explicitRoundedGrid_mulVec_intCast {d : ℕ} (jStar : ℕ) (m : Mat d) {j : ℤ} (hj : ↑jStar ≤ j) (w : Fin d → ℤ) : ∃ (w' : Fin d → ℤ), (3 ^ j • Matrix.mulVec (explicitRoundedGrid jStar m) fun (i : Fin d) => ↑(w i)) = fun (i : Fin d) => ↑(w' i)

3^j 𝒬(𝔪) maps integer vectors to integer vectors whenever j ≥ j_*.

l.source.whitney at q = 𝒬(𝔪)

theorem HCPolySupport.HighContrast.Geometry.source_whitney_roundedGrid {d jStar : ℕ} {m : Mat d} [NeZero d] (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (j : ℤ) (y : Vec d) : (∀ p ∈ maximalCellPairs (adaptedCellTranslate (explicitRoundedGrid jStar m) j y) j, standardCell d p.1 p.2 ⊆ adaptedCellTranslate (explicitRoundedGrid jStar m) j y) ∧ ((maximalCellPairs (adaptedCellTranslate (explicitRoundedGrid jStar m) j y) j).PairwiseDisjoint fun (p : ℤ × (Fin d → ℤ)) => standardCell d p.1 p.2) ∧ MeasureTheory.volume (adaptedCellTranslate (explicitRoundedGrid jStar m) j y \ ⋃ p ∈ maximalCellPairs (adaptedCellTranslate (explicitRoundedGrid jStar m) j y) j, standardCell d p.1 p.2) = 0 ∧ ∀ r ≤ j, ∃ (hfin : (maximalCellIndices (adaptedCellTranslate (explicitRoundedGrid jStar m) j y) j r).Finite), ∑ w ∈ hfin.toFinset, (MeasureTheory.volume (standardCell d r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate (explicitRoundedGrid jStar m) j y)).toReal ≤ 12 * ↑d ^ (3 / 2) * 3 ^ (r - j)

l.source.whitney, source-shaped. Let 𝔪 > 0, q = 𝒬(𝔪), W = y + ⋄_j^q. The maximal standard aligned cubes contained in W with generations at most j are pairwise disjoint subsets of W covering W up to a null set, each generation r ≤ j has finitely many of them, and Σ_{z ∈ 𝒵_r(W)} |□_r| / |W| ≤ 12 d^{3/2} 3^{r-j}.

The Euclidean grid

The initialization uses the literal Euclidean grid (1 : Mat d), while the rounded-grid infrastructure is stated for Geometry.explicitRoundedGrid jStar m. This file records the exact identity-grid bridges used to move between those surfaces.

theorem HCPolySupport.HighContrast.Geometry.unroundedGrid_one {d : ℕ} [NeZero d] : unroundedGrid 1 = 1

The unrounded grid of the Euclidean metric is the identity.

theorem HCPolySupport.HighContrast.Geometry.explicitRoundedGrid_one {d : ℕ} [NeZero d] (jStar : ℕ) : explicitRoundedGrid jStar 1 = 1

The rounded grid of the Euclidean metric is the identity.

theorem HCPolySupport.HighContrast.Geometry.one_posDef (d : ℕ) : Matrix.PosDef 1

The Euclidean metric is positive definite.

theorem HCPolySupport.HighContrast.Geometry.isUnit_one_grid (d : ℕ) : IsUnit 1

The literal Euclidean grid is invertible.

theorem HCPolySupport.HighContrast.Geometry.adaptedCell_one {d : ℕ} (j : ℤ) : adaptedCell 1 j = standardCell d j 0

The adapted cell for the identity grid is the centered standard cell.

theorem HCPolySupport.HighContrast.Geometry.adaptedCellTranslate_one_zero {d : ℕ} (j : ℤ) : adaptedCellTranslate 1 j 0 = standardCell d j 0

The translated adapted cell at the origin is the standard cell.

theorem HCPolySupport.HighContrast.Geometry.adaptedCell_one_subset_centeredCube {d : ℕ} (j : ℤ) {jStar : ℕ} (hj : j ≤ 2 * ↑jStar) : adaptedCell 1 j ⊆ centeredCube d (2 * ↑jStar)

Identity adapted cells lie in the source window whenever their generation does.