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

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

Integrability of the recentred coarse block

This file proves that the recentred coefficients respCoeffMinus F a and respCoeffPlus F a have an integrable coarse block on the response cell, and that their annealed blocks agree with the coefficient functional respJ evaluated at them. It shows the corresponding energies respEJ^∓ and trace term respTau^+ are nonnegative, that the response mean is ordered correctly relative to the raw sample, and that the recentred energy respEhatPlus is monotone. Supporting matrix and domain-geometry facts about ellipticity under a skew correction and about the block congruence of the coarse block are proved along the way. Together these supply the response-transfer result p.response.transfer.

theorem HCPolySupport.HighContrast.Multiscale.respEhatPlus_mono {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (h : BlockMatLoewnerLE (respMean P jStar F t) (respMean P jStar F s)) : BlockMatLoewnerLE (respEhatPlus P jStar F t) (respEhatPlus P jStar F s)

The adjoint congruence is Loewner-monotone too.

theorem HCPolySupport.HighContrast.Multiscale.respMean_order_of_raw (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (ε σ Cglob Cprof Csrc Bresp : ℝ) (hε : ε ∈ Set.Ioc 0 S.eps0) (hσ : σ ∈ Set.Ioc 0 ε) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (raw : RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t) : BlockMatLoewnerLE (respMean P jStar F t) (respMean P jStar F s)

E_t <= E_s at the two selected scales, straight from the raw output: jStar < s < t and Annealed.adaptedMean_antitone (e.response.imbalance.comparison, p.response.transfer).

Congruence helpers.

The annealed identification and the pathwise ellipticity inputs are derived here from the skew-shear congruence coarseBlockMatrix_sub_skew_eq_blockCongr.

Ellipticity under a constant skew shift

From the pathwise shear congruence to the annealed block

The shear is a fixed congruence, so the entrywise integrals commute with it: both the annealed identification and the entrywise integrability of the recentred block follow from the carrier-field integrability Annealed.hasIntegrableCoarseBlock_adapted, using the skew-shear congruence coarseBlockMatrix_sub_skew_eq_blockCongr.

Passing a constant congruence through the entrywise annealing integrals

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

Matrix whose entries are the integrals of the corresponding entries of f with respect to P.

Equations

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

The pathwise inputs at an adapted cell

theorem HCPolySupport.HighContrast.Multiscale.respJ_respCoeffMinus_nonneg {d : ℕ} (q : Mat d) (hq : IsUnit q) (u : ℤ) (F : BlockMat d) (hg : matTranspose (respg F) = -respg F) (a : CoeffSpace d) (p r : Vec d) : 0 ≤ respJ q u p r (respCoeffMinus F a)

Pathwise nonnegativity of the recentred response on an adapted cell (e.response.energy.and.defect).

theorem HCPolySupport.HighContrast.Multiscale.respJ_respCoeffPlus_nonneg {d : ℕ} (q : Mat d) (hq : IsUnit q) (u : ℤ) (F : BlockMat d) (hg : matTranspose (respg F) = -respg F) (a : CoeffSpace d) (p r : Vec d) : 0 ≤ respJ q u p r (respCoeffPlus F a)

The adjoint twin.

theorem HCPolySupport.HighContrast.Multiscale.respJ_eq_respCoeffMinus {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (u : ℤ) (F : BlockMat d) (hg : matTranspose (respg F) = -respg F) (a : CoeffSpace d) (p r : Vec d) : respJ q u p r (respCoeffMinus F a) = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (coarseBlockMatrix (adaptedCell q u) (respCoeffMinus F a)) (-p, r)) - vecDot p r

AK.HC (2.15) at an adapted cell for the recentred sample a - g (p.response.transfer).

theorem HCPolySupport.HighContrast.Multiscale.respJ_eq_respCoeffPlus {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (u : ℤ) (F : BlockMat d) (hg : matTranspose (respg F) = -respg F) (a : CoeffSpace d) (p r : Vec d) : respJ q u p r (respCoeffPlus F a) = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (coarseBlockMatrix (adaptedCell q u) (respCoeffPlus F a)) (-p, r)) - vecDot p r

The adjoint twin.

The annealed identifications

theorem HCPolySupport.HighContrast.Multiscale.hasIntegrableCoarseBlock_respCell_of_raw (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hell : CoarseEllipticityDagger P γ E Ψ Kg Src) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (F : BlockMat d) (hm : Matrix.PosDef (explicitCanonicalMetric F)) (u : ℤ) : HasIntegrableCoarseBlock P (respCell jStar F u)

Carrier-field integrability at the selected cells, straight from the raw output.

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_respCoeffMinus {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) (hq : IsUnit (respGrid jStar F)) (hg : matTranspose (respg F) = -respg F) (hint : HasIntegrableCoarseBlock P (respCell jStar F u)) : annealedBlockOf P (respCell jStar F u) (respCoeffMinus F) = respEhatMinus P jStar F u

The annealed block identification for the recentred coefficient: E[A(U_u; a - g)] = G^t E[A(U_u; a)] G.

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_respCoeffPlus {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) (hq : IsUnit (respGrid jStar F)) (hg : matTranspose (respg F) = -respg F) (hint : HasIntegrableCoarseBlock P (respCell jStar F u)) : annealedBlockOf P (respCell jStar F u) (respCoeffPlus F) = respEhatPlus P jStar F u

The adjoint twin.

theorem HCPolySupport.HighContrast.Multiscale.integrable_respCoeffMinus {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) (hq : IsUnit (respGrid jStar F)) (hg : matTranspose (respg F) = -respg F) (hint : HasIntegrableCoarseBlock P (respCell jStar F u)) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix (respCell jStar F u) (respCoeffMinus F a)) α β) P

Entrywise integrability of the recentred coarse block.

theorem HCPolySupport.HighContrast.Multiscale.integrable_respCoeffPlus {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) (hq : IsUnit (respGrid jStar F)) (hg : matTranspose (respg F) = -respg F) (hint : HasIntegrableCoarseBlock P (respCell jStar F u)) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix (respCell jStar F u) (respCoeffPlus F a)) α β) P

The adjoint twin.

theorem HCPolySupport.HighContrast.Multiscale.respTauPlus_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) (hpath_s : ∀ (a : CoeffSpace d), respJ (respGrid jStar F) s (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a) = 1 / 2 * blockVecDot (respxPlus P jStar F t e) (blockMatVecMul (coarseBlockMatrix (respCell jStar F s) (respCoeffPlus F a)) (respxPlus P jStar F t e)) - vecDot (respP (respMean P jStar F t) e) (respqPlus P jStar F t e)) (hint_s : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (coarseBlockMatrix (respCell jStar F s) (respCoeffPlus F a)) α β) P) (hann_s : annealedBlockOf P (respCell jStar F s) (respCoeffPlus F) = respEhatPlus P jStar F s) (hEJ : respEJPlus P jStar F t e = 1 / 2 * respLsqPlus P jStar F t e - 1) (hpq : vecDot (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) = 1) : respTauPlus P jStar F s t e = 1 / 2 * blockVecDot (respxPlus P jStar F t e) (blockMatVecMul (respEhatPlus P jStar F s) (respxPlus P jStar F t e)) - 1 / 2 * respLsqPlus P jStar F t e

The defect at the plus load, conditional on the bridge inputs at the scale s.

theorem HCPolySupport.HighContrast.Multiscale.zero_le_respTauPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) (hLoew : BlockMatLoewnerLE (respEhatPlus P jStar F t) (respEhatPlus P jStar F s)) (hτ : respTauPlus P jStar F s t e = 1 / 2 * blockVecDot (respxPlus P jStar F t e) (blockMatVecMul (respEhatPlus P jStar F s) (respxPlus P jStar F t e)) - 1 / 2 * respLsqPlus P jStar F t e) : 0 ≤ respTauPlus P jStar F s t e

The plus defect is nonnegative once Ehat_t^+ <= Ehat_s^+.

The side condition hM

Analysis.swapConj_lowerRight exposes (schurSigma E)⁻¹ as the lower-right block of the swap conjugate, so posDef_lowerRight applied there gives schurSigma E positive definite.