High-contrast homogenization: Provider.Sharp.CoarseBlockPositivity

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

The pathwise positivity of the coarse response, and the annealed sharp order

The variational coarse block response 𝐀(U; a) of s.introduction is positive definite along every realization of the coefficient field, on every nondegenerate bounded open convex domain. This is the deterministic coarse-graining theory of such a domain read on the response: the doubled quadratic form splits over the Schur data as

½ P · 𝐀(U) P = ½ p · σ(U) p + ½ r · σ_*(U)⁻¹ r, r = q - κ(U) p,

both corner matrices are positive definite -- σ_* because it is the Hessian of the flux problem and σ because it dominates σ_* -- and the two halves of the splitting vanish together only at the zero doubled vector. Nothing beyond nonemptiness of the domain enters, and no dimension is excluded.

The statement is recorded here in the shape the sharp order of the elementary block bounds is stated in, over a domain of positive volume, so that the two pathwise facts about the response can be read together. Read together they discharge both sample hypotheses of the annealed primal-adjoint order on the paper's own random matrix: positive definiteness of the annealed block, integrability of the pathwise sharp, and the annealed order 𝐀_bar(U)^♯ ≤ 𝐀_bar(U) itself all hold on every bounded open convex domain of positive volume, under the printed integrability assumption E|𝐀(U)| < ∞ alone.

The pathwise positivity clause

theorem HCPolySupport.HighContrast.Sharp.blockPosDef_coarseBlock_of_volume_pos {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (a : CoeffSpace d) : Book.Ch02.BlockPosDef (coarseBlock U a)

The coarse block response is positive definite along every realization, on a bounded open convex domain of positive volume. Positivity of the volume is used only through nonemptiness of the domain, which is the sole nondegeneracy the deterministic theory asks for.

The consequences for the annealed block

theorem HCPolySupport.HighContrast.Sharp.blockPosDef_annealedBlock_of_volume_pos {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (hint : HasIntegrableCoarseBlock P U) : Book.Ch02.BlockPosDef (annealedBlock P U)

The annealed block is positive definite on a bounded open convex domain of positive volume, as soon as the coarse response is integrable over the law: positivity holds at every sample and survives the expectation. This is the well-formedness that the annealed contrast of e.Theta.m presupposes.

The annealed sharp order on the coarse response

theorem HCPolySupport.HighContrast.Sharp.blockSharp_annealedBlock_le_of_volume_pos {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (hint : HasIntegrableCoarseBlock P U) : BlockMatLoewnerLE (blockSharp (annealedBlock P U)) (annealedBlock P U)

The annealed primal-adjoint order, on the coarse block response of the paper and over a bounded open convex domain of positive volume: the annealed block dominates its own sharp. Both hypotheses on the sample -- pathwise positive definiteness and the pathwise elementary block bounds -- are theorems here, so the printed integrability assumption E|𝐀(U)| < ∞ is the only hypothesis on the law.

theorem HCPolySupport.HighContrast.Sharp.blockSharp_annealedBlock_le_of_nonempty {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (hint : HasIntegrableCoarseBlock P U) : BlockMatLoewnerLE (blockSharp (annealedBlock P U)) (annealedBlock P U)

The annealed sharp order on a nonempty bounded open convex domain: the form in which it is consumed, the positivity of the volume being that of a nonempty open set.

theorem HCPolySupport.HighContrast.Sharp.blockSharp_annealedBlock_le_centeredCube {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (m : ℤ) (hint : HasIntegrableCoarseBlock P (centeredCube d m)) : BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d m))) (annealedBlock P (centeredCube d m))

The annealed sharp order on the centered triadic cube □_m, the carrier the annealed contrast Θ_m of e.Theta.m is read on.