High-contrast homogenization: Provider.Quenched.UnitRangeGridCount

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

The scale-n cubes centred in □_m

The concentration-for-sums condition supplied by unit range of dependence is stated for the family of standard aligned cubes of scale n whose centres lie in □_m, and its fluctuation scale is 3^(-ν(m-n)) with ν = d/2. This file identifies that family as an explicit finite index set and counts it: there are 3^(d(m-n)) such cubes, so the reciprocal square root of their number is exactly 3^(-ν(m-n)).

The count is elementary. A centre 3^n w lies in □_m exactly when each coordinate of w is strictly between ±3^(m-n)/2; since 3^(m-n) is an odd integer 2h+1, that is exactly |w i| ≤ h, and each coordinate therefore ranges over 2h + 1 = 3^(m-n) values.

The half width

def HCPolySupport.HighContrast.Quenched.centredHalfWidth (n m : ℤ) : ℤ

The largest index coordinate of a scale-n cube centred in □_m.

Equations

• HCPolySupport.HighContrast.Quenched.centredHalfWidth n m = (3 ^ (m - n).toNat - 1) / 2

theorem HCPolySupport.HighContrast.Quenched.two_mul_half_add_one (k : ℕ) : 2 * ((3 ^ k - 1) / 2) + 1 = 3 ^ k

3^k is odd, in the form the count uses.

theorem HCPolySupport.HighContrast.Quenched.two_mul_centredHalfWidth_add_one (n m : ℤ) : 2 * centredHalfWidth n m + 1 = 3 ^ (m - n).toNat

theorem HCPolySupport.HighContrast.Quenched.centredHalfWidth_nonneg (n m : ℤ) : 0 ≤ centredHalfWidth n m

The index set

def HCPolySupport.HighContrast.Quenched.centredIndexFinset (d : ℕ) (n m : ℤ) : Finset (Fin d → ℤ)

The indices of the standard aligned cubes of scale n whose centres lie in □_m.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.mem_centredIndexFinset {d : ℕ} {n m : ℤ} {w : Fin d → ℤ} : w ∈ centredIndexFinset d n m ↔ ∀ (i : Fin d), -centredHalfWidth n m ≤ w i ∧ w i ≤ centredHalfWidth n m

theorem HCPolySupport.HighContrast.Quenched.mem_centredIndexFinset_iff {d : ℕ} {n m : ℤ} (hnm : n ≤ m) {w : Fin d → ℤ} : w ∈ centredIndexFinset d n m ↔ standardCellCenter n w ∈ centeredCube d m

The index set is exactly the centring condition.

The count

theorem HCPolySupport.HighContrast.Quenched.card_centredIndexFinset (d : ℕ) (n m : ℤ) : (centredIndexFinset d n m).card = 3 ^ (d * (m - n).toNat)

There are 3^(d(m-n)) standard aligned cubes of scale n centred in □_m.

theorem HCPolySupport.HighContrast.Quenched.centredIndexFinset_nonempty (d : ℕ) (n m : ℤ) : (centredIndexFinset d n m).Nonempty

theorem HCPolySupport.HighContrast.Quenched.sqrt_card_centredIndexFinset (d : ℕ) {n m : ℤ} (hnm : n ≤ m) : √↑(centredIndexFinset d n m).card = 3 ^ (↑d / 2 * (↑m - ↑n))

The fluctuation scale of the family is 3^(ν(m-n)) with ν = d/2.

The printed form of the concentration estimate