High-contrast homogenization: Provider.Response.CutoffOscillation

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

Oscillation on an adapted child cell

The reference-coordinate gradient estimate controls the variation of the physical cutoff between the images of two points in any scale-s child cube. This is the form consumed by the cutoff-energy estimate.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_oscillation {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {R : TriadicCube d} {s t H : ℤ} (hR : R.scale = s) (hH : H = t - s) {x y : Vec d} (hx : x ∈ cubeSet R) (hy : y ∈ cubeSet R) : ‖adaptedPreYoungCutoff q hq t (matVecMul q x) - adaptedPreYoungCutoff q hq t (matVecMul q y)‖ ≤ 1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2 * 3 ^ (-H)

On a scale-s reference child, the physical cutoff pulled through q oscillates by at most the common cutoff constant times 3⁻ᴴ.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_sub_cubeAverage {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {R : TriadicCube d} {s t H : ℤ} (hR : R.scale = s) (hH : H = t - s) {x : Vec d} (hx : x ∈ cubeSet R) : |(cubeAverage R fun (z : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q z)) - adaptedPreYoungCutoff q hq t (matVecMul q x)| ≤ 1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2 * 3 ^ (-H)

The child average differs from the cutoff by the same scale-gap bound at every point of the reference child.