High-contrast homogenization: Provider.Response.AnnealedVanishing

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

The annealed vanishing of the cutoff-weighted child responses

The cutoff-weighted child responses are the one term of the cutoff-energy estimate that is not an estimate. For a single coefficient sample they do not vanish: the cutoff really does suppress the energy of the children near the boundary of the parent. They vanish only after averaging over a law that is invariant under the integer translations, because then the annealed response of a child depends on the child only through its scale, while the childwise cutoff weights average to zero against a cutoff of mean one.

This module isolates that argument. The measure-theoretic half is unconditional. The invariance half is reduced to one pathwise covariance statement — that the response on a child is the response on the base child at a translated sample — which is the shape the alignment of the grid supplies.

The childwise cutoff weights average to zero

theorem HCPolySupport.HighContrast.Response.descendantsAverage_const {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) : (descendantsAverage Q j fun (x : TriadicCube d) => c) = c

A constant descendant average is that constant.

theorem HCPolySupport.HighContrast.Response.descendantsAverage_one_sub_cubeAverage_eq_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) {φ : Vec d → ℝ} (hφ : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hmean : cubeAverage Q φ = 1) : (descendantsAverage Q j fun (R : TriadicCube d) => 1 - cubeAverage R φ) = 0

The childwise weights of a cutoff of mean one average to zero.

Integer translations preserve annealed quantities

theorem HCPolySupport.HighContrast.Response.integral_comp_translateCoeff {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) (z : Fin d → ℤ) {g : CoeffSpace d → ℝ} (hg : MeasureTheory.Integrable g P) : ∫ (a : CoeffSpace d), g (translateCoeff z a) ∂P = ∫ (a : CoeffSpace d), g a ∂P

Under a stationary law, precomposing with an integer translation of the coefficient space leaves the expectation unchanged.

theorem HCPolySupport.HighContrast.Response.integral_eq_of_translateCoeff_covariance {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {f g : CoeffSpace d → ℝ} {z : Fin d → ℤ} (hcov : ∀ (a : CoeffSpace d), f a = g (translateCoeff z a)) (hg : MeasureTheory.Integrable g P) : ∫ (a : CoeffSpace d), f a ∂P = ∫ (a : CoeffSpace d), g a ∂P

A quantity that is a fixed observable evaluated at a translated sample has the same expectation as that observable.

The annealed vanishing

theorem HCPolySupport.HighContrast.Response.integral_descendantsAverage_cutoffWeighted_eq_zero {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (Q : TriadicCube d) (j : ℕ) {φ : Vec d → ℝ} (J : TriadicCube d → CoeffSpace d → ℝ) (hint : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (J R) P) {c : ℝ} (hconst : ∀ R ∈ descendantsAtDepth Q j, ∫ (a : CoeffSpace d), J R a ∂P = c) (hφ : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hmean : cubeAverage Q φ = 1) : ∫ (a : CoeffSpace d), descendantsAverage Q j fun (R : TriadicCube d) => (1 - cubeAverage R φ) * J R a ∂P = 0

The cutoff-weighted child responses vanish in the mean. Only two inputs are used: the childwise expectations agree, and the cutoff has mean one on the parent.

theorem HCPolySupport.HighContrast.Response.integral_descendantsAverage_cutoffWeighted_eq_zero_of_covariance {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) (Q : TriadicCube d) (j : ℕ) {φ : Vec d → ℝ} (J : TriadicCube d → CoeffSpace d → ℝ) (R₀ : TriadicCube d) (hint : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (J R) P) (hbase : MeasureTheory.Integrable (J R₀) P) (hcov : ∀ R ∈ descendantsAtDepth Q j, ∃ (z : Fin d → ℤ), ∀ (a : CoeffSpace d), J R a = J R₀ (translateCoeff z a)) (hφ : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hmean : cubeAverage Q φ = 1) : ∫ (a : CoeffSpace d), descendantsAverage Q j fun (R : TriadicCube d) => (1 - cubeAverage R φ) * J R a ∂P = 0

The annealed vanishing under stationarity. The pathwise covariance hcov is the only geometric input: it says that the response on each child is the response on the base child evaluated at an integer-translated sample.

The signed cutoff-energy estimate and its annealed form

theorem HCPolySupport.HighContrast.Response.abs_cutoff_weighted_energy_sub_responseJ_add_cutoffWeightedChild_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (a : Book.Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) {s t H : ℤ} (hscale : Q.scale - ↑j = s) (hH : H = t - s) (p r : Vec d) (hCoeff : ∀ R ∈ descendantsAtDepth Q j, (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) : |(cubeAverage Q fun (x : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q x) * Book.Ch05.Section53.JUpperBoundWeakNorms.topHalfEnergyDensityOnCube Q (a.coeffOn Q) p r x) - Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) (a.coeffOn Q) p r + Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffWeightedChildResponseJOnFamilyAtDepth a Q 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.coeffOn Q) p r + √(descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p r)) * √(4 * Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) (a.coeffOn Q) p r + 2 * Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth a Q j p r)

The signed form of the cutoff-energy estimate: the cutoff-weighted child responses are kept on the left, so that a stationary average removes them.

theorem HCPolySupport.HighContrast.Response.abs_integral_le_of_integral_eq_zero {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {X W Y : CoeffSpace d → ℝ} (hX : MeasureTheory.Integrable X P) (hW : MeasureTheory.Integrable W P) (hY : MeasureTheory.Integrable Y P) (hbound : ∀ (a : CoeffSpace d), |X a + W a| ≤ Y a) (hzero : ∫ (a : CoeffSpace d), W a ∂P = 0) : |∫ (a : CoeffSpace d), X a ∂P| ≤ ∫ (a : CoeffSpace d), Y a ∂P

Composing a pointwise bound with a mean-zero correction: the correction disappears from the expectation.