High-contrast homogenization: Geometry.AnnealedBlockBridge

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

The annealed sharp order on the coarse block response

The annealed primal-adjoint order is proved on the flattened carrier, for an abstract random positive definite doubled matrix. The paper's own random matrix is the variational coarse block 𝐀(U; a) of s.introduction, whose average 𝐀_bar(U) is defined one scalar Bochner integral per entry. This file transports the abstract statement onto that carrier.

Two facts do the transporting. The first is that the entrywise definition of 𝐀_bar(U) really is the Bochner integral of the matrix-valued map: a matrix over a finite index type is the finite sum ∑ i, ∑ j, M i j • single i j 1 of scalar multiples of fixed single-entry matrices, so entrywise integrability is integrability, and the vector-valued integral is computed entrywise. The second is the bridge of the two block dialects, which carries the sharp involution, the Loewner order and positive definiteness across.

The integrability of the pathwise sharp is not an extra assumption. The reference proof observes that the elementary bounds for the coarse block sandwich 0 < 𝐀^♯(U) ≤ 𝐀(U), so the spectral norm of the sharp is dominated by the spectral norm of the response itself and no inverse moment is needed. What that argument still requires is measurability of the sharp, which is supplied here from measurability of the entries of the response: the entries of the inverse are the adjugate entries divided by the determinant, and both are polynomial in the entries.

Matrix-valued integrals from scalar entries

Everything in this section is generic: a matrix over a finite index type is a finite sum of scalar multiples of fixed single-entry matrices, so every entrywise hypothesis propagates to the matrix-valued map.

theorem HCPolySupport.HighContrast.matrix_eq_sum_smul_single {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) : M = ∑ i : n, ∑ j : n, M i j • Matrix.single i j 1

A matrix is the finite sum of its entries against the single-entry matrices.

theorem HCPolySupport.HighContrast.integrable_of_entries {n : Type u_1} [Fintype n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.Integrable (fun (a : Ω) => F a i j) μ) : MeasureTheory.Integrable F μ

Entrywise integrability is integrability. Read through the generic finite-product API at the coordinatewise presentation of Matrix n n ℝ, which agrees with the ambient one: a matrix over a finite index type carries the same topology and continuous extended norm as the finite product it is under the hood, which instance search does not unfold to on its own.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_of_entries {n : Type u_1} [Finite n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) : MeasureTheory.AEStronglyMeasurable F μ

Entrywise measurability is measurability.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_entry_mul {n : Type u_1} [Fintype n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F G : Ω → Matrix n n ℝ} (hF : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) (hG : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => G a i j) μ) (i j : n) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => (F a * G a) i j) μ

Entries of a product are finite sums of products of entries.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_det_of_entries {n : Type u_1} [Fintype n] [DecidableEq n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => (F a).det) μ

The determinant is a polynomial in the entries.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_adjugate_of_entries {n : Type u_1} [Fintype n] [DecidableEq n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) (i j : n) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => (F a).adjugate i j) μ

Each adjugate entry is a determinant of a matrix whose entries are entries of the original one and constants.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_inv_of_entries {n : Type u_1} [Fintype n] [DecidableEq n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) (i j : n) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => (F a)⁻¹ i j) μ

The entries of the inverse are measurable as soon as the entries are: they are the adjugate entries divided by the determinant, and division on the reals is measurable even at zero.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_conj_inv_of_entries {n : Type u_1} [Fintype n] [DecidableEq n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (L R : Matrix n n ℝ) {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => L * (F a)⁻¹ * R) μ

A two-sided constant conjugate of the inverse is measurable.

The structural sharp of a symmetric positive block

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_blockSharp {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpd : Book.Ch02.BlockPosDef H) : IsSymmetricBlockMat (blockSharp H)

The sharp of a symmetric positive definite doubled block is symmetric: on the flattened carrier it is positive definite, hence Hermitian.

theorem HCPolySupport.HighContrast.fullBlockSharp_le_of_blockMatLoewnerLE {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpd : Book.Ch02.BlockPosDef H) (h : BlockMatLoewnerLE (blockSharp H) H) : fullBlockSharp (toFullBlockMat H) ≤ toFullBlockMat H

The pathwise block order of the coarse block, transported to the flattened carrier.

theorem HCPolySupport.HighContrast.apply_le_apply_of_le {d : ℕ} {M N : FullBlockMat d} (h : M ≤ N) (p : BlockCoord d) : M p p ≤ N p p

The diagonal entries of a Loewner-ordered pair of doubled blocks inherit the order.

theorem HCPolySupport.HighContrast.abs_apply_le_half_add_diag {d : ℕ} {M : FullBlockMat d} (hM : Matrix.PosSemidef M) (p q : BlockCoord d) : |M p q| ≤ (M p p + M q q) / 2

A positive semidefinite doubled block is entrywise dominated by half the sum of its diagonal entries. The Cauchy-Schwarz inequality for the quadratic form the matrix defines, read off its 2 × 2 principal minor.

The annealed block is the Bochner integral of the response

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_coarseBlock {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) : IsSymmetricBlockMat (coarseBlock U a)

The coarse block response is symmetric at every sample.

theorem HCPolySupport.HighContrast.integrable_toFullBlockMat {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockMat (coarseBlock U a)) P

The flattened coarse response is Bochner integrable as soon as its entries are, which is what HasIntegrableCoarseBlock records.

theorem HCPolySupport.HighContrast.toFullBlockMat_annealedBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) : toFullBlockMat (annealedBlock P U) = ∫ (a : CoeffSpace d), toFullBlockMat (coarseBlock U a) ∂P

The entrywise annealed block is the Bochner integral of the flattened coarse response. This is the identity that lets the abstract form of the annealed primal-adjoint order be read on the paper's own carrier.

theorem HCPolySupport.HighContrast.integrable_fullBlockSharp_toFullBlockMat {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (hpos : ∀ (a : CoeffSpace d), Book.Ch02.BlockPosDef (coarseBlock U a)) (hsharp : ∀ (a : CoeffSpace d), BlockMatLoewnerLE (blockSharp (coarseBlock U a)) (coarseBlock U a)) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => fullBlockSharp (toFullBlockMat (coarseBlock U a))) P

The pathwise sharp is integrable, with no assumption beyond the ones the reference text already makes. The elementary bounds for the coarse block sandwich the sharp between zero and the response, so its spectral norm is dominated by that of the response; measurability comes from measurability of the entries of the response, which integrability supplies.

theorem HCPolySupport.HighContrast.blockSharp_annealedBlock_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} [MeasureTheory.IsProbabilityMeasure P] (hint : HasIntegrableCoarseBlock P U) (hpos : ∀ (a : CoeffSpace d), Book.Ch02.BlockPosDef (coarseBlock U a)) (hsharp : ∀ (a : CoeffSpace d), BlockMatLoewnerLE (blockSharp (coarseBlock U a)) (coarseBlock U a)) : BlockMatLoewnerLE (blockSharp (annealedBlock P U)) (annealedBlock P U)

The annealed primal-adjoint order, on the coarse block of the paper: the annealed block dominates its own sharp.

The two hypotheses on the sample are properties of the variational coarse block that s.introduction takes from HC, and are not proved in this repository: hpos is positive definiteness of the coarse response along every realization, and hsharp is its pathwise block order. The remaining hypothesis hint is the printed integrability assumption E|𝐀(U)| < ∞. Symmetry of the response and of the annealed block, positive definiteness of the annealed block, and integrability of the pathwise sharp are all consequences and are not assumed.