High-contrast homogenization: Setup.Response

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

The coarse block response and the annealed block

The coarse block response 𝐀(U; a) taken from HC is CoarseGraining's canonical variational coarse block matrix of the sample field. This file fixes it, its annealed expectation, the intrinsic annealed contrast Θ_m of e.Theta.m, and the two well-formedness predicates the annealed block needs; and it records the facts that make the encoding honest: the response depends only on the almost everywhere class of the field, its entries are the variational quantities, it is symmetric, and its diagonal entries and basis-sum quadratic forms are nonnegative.

The coarse response

noncomputable def HCPolySupport.HighContrast.coarseBlock {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) : BlockMat d

The coarse block response 𝐀(U; a) of the paper (the variational definition of the coarse block), encoded by CoarseGraining's canonical variational coarse block matrix of the sample field.

Equations

• HCPolySupport.HighContrast.coarseBlock U a = HCPolySupport.coarseBlockMatrix U ↑↑a

noncomputable def HCPolySupport.HighContrast.annealedBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : BlockMat d

The deterministic annealed block 𝐀_bar(U) = E[𝐀(U; ·)], entrywise.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.HasIntegrableCoarseBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : Prop

Integrability of the coarse response over the law: every entry of 𝐀(U; ·) is P-integrable, so that annealedBlock P U is the expectation E[𝐀(U; ·)] of e.Theta.m.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.HasMeasurableCoarseBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : Prop

Measurability of the coarse response over the law: every entry of 𝐀(U; ·) is almost surely strongly measurable for the law.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.annealedContrast {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m : ℤ) : ℝ

The Euclidean annealed contrast Θ_m (e.Theta.m): the intrinsic contrast of the annealed block of the centered cube □_m.

Equations

• HCPolySupport.HighContrast.annealedContrast P m = HCPolySupport.HighContrast.blockContrast (HCPolySupport.HighContrast.annealedBlock P (HCPolySupport.HighContrast.centeredCube d m))

The response depends only on the almost everywhere class

theorem HCPolySupport.HighContrast.coarseBlock_eq_of_ae_eq {d : ℕ} {U : Set (Vec d)} (a : CoeffSpace d) {f : CoeffField d} (hf : ↑↑a =ᵐ[MeasureTheory.volume] f) : coarseBlock U a = coarseBlockMatrix U f

The coarse response only sees the almost everywhere class of the field: its value at any representative of the sample is the same.

theorem HCPolySupport.HighContrast.Mu_congr_ae {d : ℕ} {U : Set (Vec d)} {f h : CoeffField d} (hfh : f =ᵐ[MeasureTheory.volume] h) (Q : BlockVec d) : Mu U Q f = Mu U Q h

The variational quantity only sees the almost everywhere class of the field.

Entries, symmetry, nonnegativity

theorem HCPolySupport.HighContrast.blockMatEntry_coarseBlockMatrix {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (α β : BlockCoord d) : blockMatEntry (coarseBlockMatrix U a) α β = if α = β then 2 * Mu U (blockBasis α) a else Mu U (blockBasis α + blockBasis β) a - Mu U (blockBasis α) a - Mu U (blockBasis β) a

The entries of the coarse block response, in terms of the variational quantity.

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_coarseBlockMatrix {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : IsSymmetricBlockMat (coarseBlockMatrix U a)

The coarse block response is a symmetric doubled matrix.

theorem HCPolySupport.HighContrast.zero_le_Mu_coeffSpace {d : ℕ} (U : Set (Vec d)) (Q : BlockVec d) (a : CoeffSpace d) : 0 ≤ Mu U Q ↑↑a

On the coefficient space the variational quantity of the coarse block problem is nonnegative: every admissible competitor has nonnegative energy, so the infimum is nonnegative even where the Bochner integral is a junk value.

theorem HCPolySupport.HighContrast.zero_le_blockMatEntry_coarseBlock_diag {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) (γ : BlockCoord d) : 0 ≤ blockMatEntry (coarseBlock U a) γ γ

Diagonal entries of the coarse response are nonnegative.

theorem HCPolySupport.HighContrast.zero_le_blockVecDot_coarseBlock_blockBasis_add {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) (α β : BlockCoord d) : 0 ≤ blockVecDot (blockBasis α + blockBasis β) (blockMatVecMul (coarseBlock U a) (blockBasis α + blockBasis β))

The doubled quadratic form of the coarse response is nonnegative on the sums of two basis vectors, these being the vectors that control its entries.

The annealed block is the entrywise expectation

theorem HCPolySupport.HighContrast.blockMatEntry_annealedBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) (α β : BlockCoord d) : blockMatEntry (annealedBlock P U) α β = ∫ (a : CoeffSpace d), blockMatEntry (coarseBlock U a) α β ∂P

Entries of the annealed block are the expectations of the entries of the coarse response.

theorem HCPolySupport.HighContrast.blockVecDot_blockMatVecMul_annealedBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (X : BlockVec d) : blockVecDot X (blockMatVecMul (annealedBlock P U) X) = ∫ (a : CoeffSpace d), blockVecDot X (blockMatVecMul (coarseBlock U a) X) ∂P

The annealed quadratic form is the expectation of the sample quadratic form, at every doubled vector, whenever the coarse response is integrable over the law. This is the identity that pins annealedBlock to E[𝐀(U; ·)].

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

The positivity of the annealed block. The expectation of an integrable family of positive definite coarse responses is positive definite: this is the well-formedness that e.Theta.m presupposes for Θ_m.