High-contrast homogenization: Provider.Response.CutoffEnergy

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

The cutoff-energy estimate

Inserting a mean-one cutoff into the parent energy changes it by two terms: the childwise oscillation of the cutoff against the parent energy density, and the mean defect of the cutoff against the childwise parent energies. The first is controlled by the cutoff's adapted-coordinate gradient alone, and the sharper first-derivative coefficient of the adapted construction gives it the dimensional size 32 d² K₀ 3^{-H}, where K₀ is the derivative bound of the one-dimensional transition profile and H is the gap between the parent scale and the child scale.

The identity below is exact and the oscillation bound is unconditional; the mean-defect term is carried as an explicit bound, since controlling it is a separate step of the localization argument.

The sharper oscillation of the adapted cutoff

theorem HCPolySupport.HighContrast.Response.sharpCutoffCoefficient_nonneg (d : ℕ) : 0 ≤ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound

The sharp dimensional coefficient of the adapted cutoff's first derivative is nonnegative.

theorem HCPolySupport.HighContrast.Response.exists_one_le_sharpCutoffConstant (d : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound ≤ C

A dimension-only constant at least one that dominates the cutoff's first-derivative coefficient. This is the form in which the coefficient leaves the analytic layer: it depends on the dimension alone, and it is selected before any probability law, grid, scale, coefficient, centre, or load.

theorem HCPolySupport.HighContrast.Response.rpow_neg_natCast_eq_zpow_neg (H : ℕ) : 3 ^ (-↑H) = 3 ^ (-↑H)

The scale-gap factor written with a natural exponent, as the mixed extended-real assembly reads it, agrees with the integer-exponent form used by the analytic estimates.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_oscillation_sharp {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)‖ ≤ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-H)

On a scale-s reference child the physical cutoff pulled through the grid matrix oscillates by at most the sharp dimensional coefficient times the scale gap.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_sub_cubeAverage_sharp {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)| ≤ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-H)

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

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_sub_cubeAverage_sharp_ae {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) ∂volumeMeasureOn (cubeSet R), |(cubeAverage R fun (z : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q z)) - adaptedPreYoungCutoff q hq t (matVecMul q x)| ≤ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-H)

The a.e. form of the sharp child-average oscillation bound.

theorem HCPolySupport.HighContrast.Response.abs_cutoffOscillationTermOnCubeAtDepth_adaptedPreYoungCutoff_le_sharp {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (Q : TriadicCube d) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) (j : ℕ) {s t H : ℤ} (hscale : Q.scale - ↑j = s) (hH : H = t - s) (p r : Vec d) : |Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffOscillationTermOnCubeAtDepth Q a j (fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) p r| ≤ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-H) * Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) a p r

The cutoff-energy oscillation term carries the sharp dimensional coefficient and the scale gap.

The cutoff-energy split

theorem HCPolySupport.HighContrast.Response.cubeAverage_topHalfEnergyDensityOnCube_eq_responseJ {d : ℕ} (Q : TriadicCube d) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) (p r : Vec d) : cubeAverage Q (Book.Ch05.Section53.JUpperBoundWeakNorms.topHalfEnergyDensityOnCube Q a p r) = Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) a p r

The parent energy density averages to the parent response.

theorem HCPolySupport.HighContrast.Response.descendantsAverage_add {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F G : TriadicCube d → ℝ) : descendantsAverage Q j F + descendantsAverage Q j G = descendantsAverage Q j fun (R : TriadicCube d) => F R + G R

Descendant averages are additive.

theorem HCPolySupport.HighContrast.Response.cutoffOscillationTerm_add_meanDefectTopEnergyTerm_eq {d : ℕ} (Q : TriadicCube d) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) (j : ℕ) {φ : Vec d → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn (cubeSet Q))) (hbdd : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet Q), ‖φ x‖ ≤ 2) (p r : Vec d) : Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffOscillationTermOnCubeAtDepth Q a j φ p r + Book.Ch05.Section53.JUpperBoundWeakNorms.meanDefectTopEnergyTermOnCubeAtDepth Q a j φ p r = Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) a p r - cubeAverage Q fun (x : Vec d) => φ x * Book.Ch05.Section53.JUpperBoundWeakNorms.topHalfEnergyDensityOnCube Q a p r x

The cutoff-energy split. Inserting a cutoff into the parent energy changes it by exactly the childwise oscillation term plus the mean-defect term.