High-contrast homogenization: Entry.Response.Rows.AnnealedBlockMeanCancellation

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

Mean Cancellation and Full Stationarity of the Annealed Block

Above the stationarity threshold j_*, the cell mean of a subcell's own doubled optimizer state has the form x + R 𝐀(V) x with a common annealed block 𝐀, so the weighted flat average, over the coarse subcells of the terminal cell, of the annealed cell means of each subcell's own optimizer state vanishes once the flat weights are normalized. Because the crossed pairing is bilinear and both the finite flat average and the expectation are linear, pairing that flat average against the dual variable Y is the expectation of the weighted flat average of the pathwise crossed pairings. For a stationary law and a scale above j_*, this file also shows the whole annealed coarse block of a recentred family — diagonal and off-diagonal alike — is the same 2d-by-2d matrix at every aligned cell of the generation, since every such cell is an integer translate of the centred one and the recentring commutes with translation. Both the cancellation of the weighted flat average of the annealed cell means and the cell-independence of the annealed coarse block are used in the cell half of the cutoff-mean row of p.response.transfer.

The constant cell means cancel after expectation

In the cell half of the cutoff-mean row of p.response.transfer, the weighted flat average, over the coarse subcells of the terminal cell, of the ANNEALED cell means of each subcell's own optimizer state vanishes. Above the scale j_* the subcells are integer translates of one another and the law is stationary, so the annealed block of every subcell agrees; the pathwise cell mean of the optimizer state is x + R 𝐀 x (AK.HC (2.32)), and its expectation is x + R 𝐀_bar x with the common annealed block 𝐀_bar. The weights — the subcell means of the cutoff fluctuation φ - 1 — have normalized sum zero because the cutoff has mean one on the terminal cell.

theorem HCPolySupport.HighContrast.Multiscale.avsum_weighted_integral_cellAverage_subcellOptimizer_eq_zero {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (jStar : ℕ) (F : BlockMat d) (H : ℕ) (s t : ℤ) (e : Vec d) (φ : Vec d → ℝ) (hq : IsUnit (respGrid jStar F)) (hφ : IsResponseCutoff (respGrid jStar F) t φ) (ht : t = s + ↑H) (Mv : (Fin d → ℤ) → CoeffSpace d → BlockVec d) (A : BlockMat d) (hMv : ∀ w ∈ triadicIndexBox d H, ∀ (a : CoeffSpace d), Mv w a = blockResponseMean (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)) (-respP (respMean P jStar F t) e, respqMinus P jStar F t e)) (hann : ∀ w ∈ triadicIndexBox d H, annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F) = A) (hint : ∀ w ∈ triadicIndexBox d H, ∀ (i : Fin d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => (Mv w a).1 i) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => (Mv w a).2 i) P) (hblkint : ∀ w ∈ triadicIndexBox d H, HasIntegrableCoarseBlock P (adaptedCellAtCenter (respGrid jStar F) s w)) (hquad : ∀ w ∈ triadicIndexBox d H, ∀ (a : CoeffSpace d), HasQuadraticMu (adaptedCellAtCenter (respGrid jStar F) s w) ↑↑a) : (∀ (i : Fin d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * ∫ (a : CoeffSpace d), (Mv w a).1 i ∂P = 0) ∧ ∀ (i : Fin d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * ∫ (a : CoeffSpace d), (Mv w a).2 i ∂P = 0

The weighted cell means of the subcell optimizers cancel, negative sign. In the cell half of the cutoff-mean row of p.response.transfer, let the cell mean of the doubled optimizer state of each coarse subcell U_w of the terminal cell U_t be the block response of the recentred coefficient a_- = a - g at the load x^- = (-p, q^-), with a common annealed block A above j_*. Then the normalized sum, over the subcells, of the subcell mean of φ - 1 times the expectation of each coordinate of that optimizer mean is zero. The expectation of x^- + R 𝐀 x^- is x^- + R A x^- at every subcell by integral_blockResponseMean, because the subcell's annealed block is A; the weights have normalized sum zero by avsum_volumeAverage_sub_one_eq_zero, the cutoff having mean one.

theorem HCPolySupport.HighContrast.Multiscale.avsum_weighted_integral_cellAverage_subcellOptimizerPlus_eq_zero {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (jStar : ℕ) (F : BlockMat d) (H : ℕ) (s t : ℤ) (e : Vec d) (φ : Vec d → ℝ) (hq : IsUnit (respGrid jStar F)) (hφ : IsResponseCutoff (respGrid jStar F) t φ) (ht : t = s + ↑H) (Mv : (Fin d → ℤ) → CoeffSpace d → BlockVec d) (A : BlockMat d) (hMv : ∀ w ∈ triadicIndexBox d H, ∀ (a : CoeffSpace d), Mv w a = blockResponseMean (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)) (-respP (respMean P jStar F t) e, respqPlus P jStar F t e)) (hann : ∀ w ∈ triadicIndexBox d H, annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F) = A) (hint : ∀ w ∈ triadicIndexBox d H, ∀ (i : Fin d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => (Mv w a).1 i) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => (Mv w a).2 i) P) (hblkint : ∀ w ∈ triadicIndexBox d H, HasIntegrableCoarseBlock P (adaptedCellAtCenter (respGrid jStar F) s w)) (hquad : ∀ w ∈ triadicIndexBox d H, ∀ (a : CoeffSpace d), HasQuadraticMu (adaptedCellAtCenter (respGrid jStar F) s w) ↑↑a) : (∀ (i : Fin d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * ∫ (a : CoeffSpace d), (Mv w a).1 i ∂P = 0) ∧ ∀ (i : Fin d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * ∫ (a : CoeffSpace d), (Mv w a).2 i ∂P = 0

The weighted cell means of the subcell optimizers cancel, adjoint sign. The adjoint twin of avsum_weighted_integral_cellAverage_subcellOptimizer_eq_zero for the recentred coefficient a_+ = aᵗ + g at the load x^+ = (-p, q^+): the normalized sum, over the coarse subcells of the terminal cell, of the subcell mean of φ - 1 times the expectation of each coordinate of the optimizer mean vanishes, for the adjoint coarse block.

The crossed pairing of a weighted flat average of expectations

The cell part of the cutoff-mean defect of p.response.transfer is a weighted flat average, over the coarse subcells of the terminal cell, of the annealed cell means of the doubled optimizer state. Because the crossed pairing is bilinear and both the finite flat average and the expectation are linear, pairing the flat average against the dual variable Y — the gradient slot against Y.2 and the flux slot against Y.1 — is the expectation of the weighted flat average of the pathwise crossed pairings.

theorem HCPolySupport.HighContrast.Multiscale.vecDot_avsum_integral_eq_integral_avsum_pairing {d : ℕ} {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (P : MeasureTheory.Measure α) (Z : Finset ι) (c : ι → ℝ) (Y : BlockVec d) (M : ι → α → BlockVec d) (N : BlockVec d) (hN1 : N.1 = fun (i : Fin d) => (↑Z.card)⁻¹ * ∑ w ∈ Z, c w * ∫ (a : α), (M w a).1 i ∂P) (hN2 : N.2 = fun (i : Fin d) => (↑Z.card)⁻¹ * ∑ w ∈ Z, c w * ∫ (a : α), (M w a).2 i ∂P) (hint1 : ∀ w ∈ Z, ∀ (i : Fin d), MeasureTheory.Integrable (fun (a : α) => (M w a).1 i) P) (hint2 : ∀ w ∈ Z, ∀ (i : Fin d), MeasureTheory.Integrable (fun (a : α) => (M w a).2 i) P) : vecDot N.1 Y.2 + vecDot Y.1 N.2 = ∫ (a : α), (↑Z.card)⁻¹ * ∑ w ∈ Z, c w * (vecDot (M w a).1 Y.2 + vecDot Y.1 (M w a).2) ∂P

The crossed pairing of a weighted flat average of expectations. Let Z be a finite index set, c a real weight, M a family of doubled vectors indexed by Z and the sample space, and let N be the doubled vector whose two slots are the weighted flat averages of the expectations of the corresponding slots of M. Then the crossed pairing of N against Y (gradient slot against Y.2, flux slot against Y.1) equals the expectation of the weighted flat average of the pathwise crossed pairings. This is the exchange of the finite average with the expectation used in p.response.transfer.

The whole annealed block of an aligned cell is cell-independent

For a stationary law P and a scale j above j_*, every aligned cell of the generation is an integer translate of the centred adapted cell, the law is invariant under integer translations, and the recentring of p.response.transfer subtracts (respectively adds) a constant matrix field, which commutes with translation. Consequently the whole annealed block of the recentred field a_- = a - g or a_+ = aᵀ + g is the same 2d-by-2d matrix at every cell of the generation.

StationaryAnnealedErrorScalars records this for the two diagonal sub-blocks only. The mean cancellation of p.response.transfer — "the constant cell means cancel after expectation, because the scale-s translations are integral" — needs the whole block, because the annealed cell mean of the optimizer state is x + R 𝐀 x and the off-diagonal sub-blocks enter it. This file supplies the off-diagonal half and packages the four fields into a single block equality.

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_adaptedCellAtCenter_respCoeffMinus_eq_full {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (m : Mat d) (F : BlockMat d) (j : ℤ) (hj : ↑jStar ≤ j) (w : Fin d → ℤ) (hmeas : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) (respCoeffMinus F a)) α β) P) : annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) j w) (respCoeffMinus F) = annealedBlockOf P (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) (respCoeffMinus F)

The whole annealed block of the recentred field is the same on every aligned cell, minus sign. For a stationary law P and the recentred coefficient a_- = a - g of p.response.transfer, the P-entrywise annealed block of the pathwise coarse block on an aligned cell of scale j ≥ j_* is the annealed block of the centred cell, independently of the cell index w. This is the full BlockMat form, off-diagonal sub-blocks included.

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_adaptedCellAtCenter_respCoeffPlus_eq_full {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (m : Mat d) (F : BlockMat d) (j : ℤ) (hj : ↑jStar ≤ j) (w : Fin d → ℤ) (hmeas : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) (respCoeffPlus F a)) α β) P) : annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) j w) (respCoeffPlus F) = annealedBlockOf P (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) (respCoeffPlus F)

The whole annealed block of the recentred field is the same on every aligned cell, plus sign. For a stationary law P and the recentred coefficient a_+ = aᵀ + g of p.response.transfer, the P-entrywise annealed block of the pathwise coarse block on an aligned cell of scale j ≥ j_* is the annealed block of the centred cell, independently of the cell index w. This is the full BlockMat form, off-diagonal sub-blocks included.