High-contrast homogenization: Provider.Response.DiagonalWeakNormVariance

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

Finite variance on an aligned scale

The child averages at a fixed scale have the parent average as their ordinary finite mean. Subtracting that mean can therefore only decrease their normalized Euclidean square sum. This is the variance step in the scale-by-scale energy bound of the weak-norm estimate.

theorem HCPolySupport.HighContrast.Response.avsum_sq_sub_mean_eq {ι : Type u_1} {Z : Finset ι} (hZ : Z.Nonempty) (f : ι → ℝ) (m : ℝ) (hmean : avsum Z f = m) : (avsum Z fun (z : ι) => (f z - m) ^ 2) = (avsum Z fun (z : ι) => f z ^ 2) - m ^ 2

The scalar finite-variance identity for the normalized average.

theorem HCPolySupport.HighContrast.Response.blockAvsumL2_sub_mean_le {d : ℕ} {ι : Type u_1} {Z : Finset ι} (hZ : Z.Nonempty) (u : ι → BlockVec d) (m : BlockVec d) (hmean : ∀ (a : BlockCoord d), (avsum Z fun (z : ι) => toFullBlockVec (u z) a) = toFullBlockVec m a) : (blockAvsumL2 Z fun (z : ι) => u z - m) ≤ blockAvsumL2 Z u

Subtracting the finite mean decreases the normalized doubled Euclidean length.