High-contrast homogenization: Entry.Response.Core.AnnealedBlockIdentity

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

The annealed block identity

This file proves the annealed block identity for the doubled optimizer state: the annealed means Y^∓, the expectations of the cell average of the doubled optimizer state, agree with the annealed block of the recentred coefficients respCoeffMinus/respCoeffPlus under the block congruence carried by the shear correction, the response-transfer identity p.response.transfer. It records the resulting integrability and symmetry of the coarse block matrix, together with the closed algebraic identities — for the full block matrix, its transpose, the matrix-valued integral matIntegral and its behaviour under left and right scalar multiplication, and the shear congruence of the coarse block — that the identification is built from.

HC bridge I, part 4 of 4: STEPs 4-5c and the annealed block conclusions

The annealed means Y^∓ are the expectations of the cell average of the doubled optimizer state, E[(X_{u_t})_{U_t}] = Y^∓.

STEP 4: the block-level shear

theorem HCPolySupport.HighContrast.Multiscale.isCoarseBlockMatrix_sub_skew {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {g : Mat d} (hg : matTranspose g = -g) (hquad : HasQuadraticMu U a) : IsCoarseBlockMatrix U (fun (x : Vec d) => a x - g) (blockCongr { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } (coarseBlockMatrix U a))

STEP 5a: moving the constant congruence through the annealing integral

noncomputable def HCPolySupport.HighContrast.Multiscale.matIntegral {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) (f : CoeffSpace d → Matrix ι ι ℝ) : Matrix ι ι ℝ

Integrate a matrix-valued function entrywise with respect to the coefficient measure P.

Equations

• HCPolySupport.HighContrast.Multiscale.matIntegral P f = Matrix.of fun (i j : ι) => ∫ (a : HCPolySupport.HighContrast.CoeffSpace d), f a i j ∂P

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_eq_blockCongr {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {V : Set (Vec d)} (G : BlockMat d) (b : CoeffSpace d → CoeffField d) (hint : HasIntegrableCoarseBlock P V) (hb : ∀ (a : CoeffSpace d), coarseBlockMatrix V (b a) = blockCongr G (coarseBlock V a)) : annealedBlockOf P V b = blockCongr G (annealedBlock P V)

The annealed block of a constant congruence of the pathwise block is the congruence of the annealed block: the congruence has constant coefficients, so it passes through the integral.

STEP 5b

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_respCoeffMinus_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (hquad : ∀ (a : CoeffSpace d), HasQuadraticMu (respCell jStar F t) ↑↑a) (hint : HasIntegrableCoarseBlock P (respCell jStar F t)) : annealedBlockOf P (respCell jStar F t) (respCoeffMinus F) = respEhatMinus P jStar F t

The recentred annealed block is the congruence of the annealed block (p.response.transfer, Ehat_t^- = G^t E_t G with a_- = a - g): E[A(U_t; a - g)] = G^t E[A(U_t; a)] G. The hypotheses hquad and hint are needed because coarseBlockMatrix is recovered from Mu only by polarization and annealedBlockOf integrates entries.

STEP 5c

theorem HCPolySupport.HighContrast.Multiscale.blockCongr_blockCongr {d : ℕ} (G₁ G₂ A : BlockMat d) : blockCongr G₂ (blockCongr G₁ A) = blockCongr (ofFullBlockMat (toFullBlockMat G₁ * toFullBlockMat G₂)) A

Congruences compose: G₂ᵀ (G₁ᵀ A G₁) G₂ = (G₁ G₂)ᵀ A (G₁ G₂).

theorem HCPolySupport.HighContrast.Multiscale.blockCongr_blockD {d : ℕ} (A : BlockMat d) : blockCongr (blockD d) A = blockMatFlipFlux A

Congruence by D = diag(Id, -Id) is the flux sign flip of the adjoint symmetry.

theorem HCPolySupport.HighContrast.Multiscale.blockD_mul_shear_neg {d : ℕ} (g : Mat d) : toFullBlockMat (blockD d) * toFullBlockMat { upperLeft := 1, upperRight := 0, lowerLeft := -g, lowerRight := 1 } = toFullBlockMat { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } * toFullBlockMat (blockD d)

D · G_{-g} = G_g · D in the full 2d × 2d carrier: both are [[Id, 0], [g, -Id]].

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_respCoeffPlus_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (hquad : ∀ (a : CoeffSpace d), HasQuadraticMu (respCell jStar F t) ↑↑a) (hint : HasIntegrableCoarseBlock P (respCell jStar F t)) : annealedBlockOf P (respCell jStar F t) (respCoeffPlus F) = respEhatPlus P jStar F t

The adjoint twin (p.response.transfer, Ehat_t^+ = D Ehat_t^- D). The hypotheses hquad and hint are needed because coarseBlockMatrix is recovered from Mu only by polarization and annealedBlockOf integrates entries.

theorem HCPolySupport.HighContrast.Multiscale.integrable_blockMatEntry_coarseBlockMatrix_of_blockCongr {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {V : Set (Vec d)} (G : BlockMat d) {b : CoeffSpace d → CoeffField d} (hint : HasIntegrableCoarseBlock P V) (hb : ∀ (a : CoeffSpace d), coarseBlockMatrix V (b a) = blockCongr G (coarseBlock V a)) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix V (b a)) α β) P

AUX (helper, NEW). If the pathwise block of a recentred field family is a CONSTANT congruence Gᵀ 𝐀(V; a) G of the pathwise coarse block, then each of its entries is a fixed real linear combination of the entries of 𝐀(V; ·), hence P-integrable by HasIntegrableCoarseBlock. This is the integrability input of integral_blockResponseMean.

theorem HCPolySupport.HighContrast.Multiscale.integral_blockResponseMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (V : Set (Vec d)) (b : CoeffSpace d → CoeffField d) (x : BlockVec d) (hA : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix V (b a)) α β) P) : (fun (i : Fin d) => ∫ (a : CoeffSpace d), (blockResponseMean (coarseBlockMatrix V (b a)) x).1 i ∂P, fun (i : Fin d) => ∫ (a : CoeffSpace d), (blockResponseMean (coarseBlockMatrix V (b a)) x).2 i ∂P) = blockResponseMean (annealedBlockOf P V b) x

AUX (helper, NEW). blockResponseMean A x is affine-linear in A for fixed x, so with entrywise integrability of a ↦ 𝐀(V; b a) the entrywise annealing integral passes through it: (∫ (·)₁, ∫ (·)₂) = blockResponseMean (annealedBlockOf P V b) x. P is a probability measure, so the constant term x survives the integral unchanged.