High-contrast homogenization: Provider.Recurrence.RoundedGrid

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

The rounded adapted grid

The rounded adapted grid of a metric replaces a positive symmetric matrix m by the entrywise rounding

Q_ℓ(m) = 3^{-ℓ} ⌈3^ℓ 𝓛(m)⌉, 𝓛(m) := |m^{-1}|^{1/2} m^{1/2},

at an alignment scale ℓ ≥ k_0(d). Two properties of that convention are what the adapted geometry rests on, and both are proved here.

The first is that Q_ℓ(m) is again positive. The eigenvalues of the normalized square root 𝓛(m) are the numbers (λ_i(m)/λ_min(m))^{1/2} ≥ 1, so 𝓛(m) ≥ I; rounding moves each entry by less than 3^{-ℓ}, and the spectral norm of a d × d matrix is at most d times the largest absolute value of its entries, so the rounding perturbs the quadratic form by at most d 3^{-ℓ} ≤ d 3^{-k_0(d)}. This is exactly the quantity the choice of k_0(d) controls, and kZero_spec bounds it by 1/101. Hence Q_ℓ(m) stays positive definite, and the adapted cells ⋄_j^q = q□_j are genuine cells.

The second is integrality. Every entry of Q_ℓ(m) is 3^{-ℓ} times an integer, so for every scale j ≥ ℓ the matrix 3^j Q_ℓ(m) has integer entries and the aligned translation vectors 3^j q w, w ∈ ℤ^d, lie in ℤ^d. That is the integrality clause of the aligned subdivision in the coarse-block properties taken from HC, and it is what lets stationarity be applied to the child cells.

The normalized square root

theorem HCPolySupport.HighContrast.Recurrence.matSqrt_smul {d : ℕ} {c : ℝ} (hc : 0 ≤ c) {m : Mat d} (hm : Matrix.PosSemidef m) : matSqrt (c • m) = √c • matSqrt m

The square root of a nonnegative multiple of a positive semidefinite matrix scales by the square root of the multiple.

theorem HCPolySupport.HighContrast.Recurrence.matSqrt_one {d : ℕ} : matSqrt 1 = 1

The identity is its own square root.

theorem HCPolySupport.HighContrast.Recurrence.one_le_specBound_inv_smul {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : 1 ≤ specBound m⁻¹ • m

The normalization of the rounded adapted grid is at least the identity. Scaling a positive definite matrix by |m^{-1}| puts it above the identity: conjugating m^{-1} ≤ |m^{-1}| I by m^{1/2} gives I ≤ |m^{-1}| m.

theorem HCPolySupport.HighContrast.Recurrence.one_le_normalized_matSqrt {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : 1 ≤ √(specBound m⁻¹) • matSqrt m

The normalized square root is at least the identity. Its eigenvalues are the numbers (λ_i(m)/λ_min(m))^{1/2}, the least of which is one.

theorem HCPolySupport.HighContrast.Recurrence.normalized_matSqrt_symm {d : ℕ} {m : Mat d} (hm : Matrix.PosSemidef m) (i k : Fin d) : √(specBound m⁻¹) * matSqrt m k i = √(specBound m⁻¹) * matSqrt m i k

The normalized square root is symmetric.

Rounding moves each entry by less than 3^{-ℓ}

theorem HCPolySupport.HighContrast.Recurrence.roundedGrid_apply {d : ℕ} (j : ℤ) (m : Mat d) (i k : Fin d) : roundedGrid j m i k = 3 ^ (-j) * ↑⌈3 ^ j * (√(specBound m⁻¹) * matSqrt m i k)⌉

The entries of the rounded grid, in terms of the normalized square root.

theorem HCPolySupport.HighContrast.Recurrence.roundedGrid_sub_normalized_matSqrt_mem {d : ℕ} (j : ℤ) (m : Mat d) (i k : Fin d) : 0 ≤ roundedGrid j m i k - √(specBound m⁻¹) * matSqrt m i k ∧ roundedGrid j m i k - √(specBound m⁻¹) * matSqrt m i k ≤ 3 ^ (-j)

The rounding error of the rounded adapted grid. Every entry of Q_ℓ(m) - 𝓛(m) is nonnegative and at most 3^{-ℓ}.

theorem HCPolySupport.HighContrast.Recurrence.roundedGrid_symm {d : ℕ} (j : ℤ) {m : Mat d} (hm : Matrix.PosSemidef m) (i k : Fin d) : roundedGrid j m k i = roundedGrid j m i k

The rounded grid is symmetric.

Positivity of the rounded grid

theorem HCPolySupport.HighContrast.Recurrence.neg_le_dotProduct_mulVec_of_abs_entry_le {d : ℕ} {E : Mat d} {delta : ℝ} (hE : ∀ (i k : Fin d), |E i k| ≤ delta) (x : Fin d → ℝ) : -(delta * ↑d * ∑ i : Fin d, x i * x i) ≤ x ⬝ᵥ Matrix.mulVec E x

The quadratic form of a matrix with small entries is small: the entrywise bound δ gives |x · E x| ≤ dδ|x|², the spectral-norm-by-entries estimate the reference text uses on the rounding error.

theorem HCPolySupport.HighContrast.Recurrence.posDef_roundedGrid {d : ℕ} {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) : Matrix.PosDef (roundedGrid l m)

The rounded grid is positive definite. This is where the choice of k_0(d) is used: at an alignment ℓ ≥ k_0(d) the rounding error d 3^{-ℓ} is at most the 1/101 of kZero_spec, which the normalization 𝓛(m) ≥ I absorbs.

theorem HCPolySupport.HighContrast.Recurrence.posDef_of_isRoundedGrid {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) : Matrix.PosDef q

A rounded adapted grid is positive definite.

Integrality of the aligned translations

theorem HCPolySupport.HighContrast.Recurrence.exists_int_roundedGrid {d : ℕ} (l : ℤ) (m : Mat d) (i k : Fin d) : ∃ (c : ℤ), roundedGrid l m i k = 3 ^ (-l) * ↑c

Every entry of the rounded grid is 3^{-ℓ} times an integer.

theorem HCPolySupport.HighContrast.Recurrence.exists_int_zpow_smul_of_isRoundedGrid {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) : ∃ (n : Fin d → Fin d → ℤ), ∀ (i k : Fin d), 3 ^ j * q i k = ↑(n i k)

3^j q has integer entries at every scale at or above the alignment. This is the integrality clause of the aligned subdivision in the coarse-block properties taken from HC.

theorem HCPolySupport.HighContrast.Recurrence.exists_intVec_adaptedCellCenter {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (w : Fin d → ℤ) : ∃ (v : Fin d → ℤ), adaptedCellCenter q j w = fun (i : Fin d) => ↑(v i)

The aligned translation vectors are integral. For a rounded grid at alignment ℓ and any scale j ≥ ℓ, the center 3^j q w of an aligned adapted cell lies in ℤ^d.