High-contrast homogenization: Provider.Response.ProfileWeakConstant

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

Constant fields in the scale-average seminorm

The normalized seminorm of a constant doubled vector is its Euclidean length times the geometric scale sum. This identifies exactly the constant contribution that appears when a random cell average is replaced by its annealed center.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_const_adapted {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (z : Fin d → ℤ) (c : BlockVec d) : (blockCellAverage (adaptedCellAt q k z) fun (x : Vec d) => c) = c

A constant doubled field has the same average on every adapted cell.

theorem HCPolySupport.HighContrast.Response.tsum_rpow_three_neg_half_eq_constantSeminormCoefficient : ∑' (j : ℕ), 3 ^ (-(1 / 2 * ↑j)) = constantSeminormCoefficient

The half-order scale weights sum to the constant coefficient.

theorem HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_const {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (c : BlockVec d) : (ENNReal.ofReal (3 ^ (-(1 / 2 * ↑t))) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => c) = ENNReal.ofReal constantSeminormCoefficient * ENNReal.ofReal √(blockVecDot c c)

The exact normalized seminorm of a constant doubled field.

theorem HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_blockDiag_const {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {m : Mat d} (hm : Matrix.PosDef m) (t : ℤ) (c : BlockVec d) : (ENNReal.ofReal (3 ^ (-(1 / 2 * ↑t))) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag (matSqrt m) (matSqrt m)⁻¹) c) = ENNReal.ofReal constantSeminormCoefficient * ENNReal.ofReal √(metricBlockNormSq m c)

The exact constant-field identity in the canonical diagonal metric.