High-contrast homogenization: Annealed.Contrast

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

The annealed contrast in printed form

The reference text writes the annealed contrast Θ_m of e.Theta.m as a minimum over skew matrices h of the conjugated norms |σ_bar_*^{-1/2} (σ_bar + (k_bar - h)ᵗ σ_bar_*⁻¹ (k_bar - h)) σ_bar_*^{-1/2}|, the Schur data being that of the annealed block 𝐀_bar(□_m). The encoding annealedContrast is instead the Loewner-scaling infimum, and the identification of the two is available on symmetric positive definite doubled blocks.

This file supplies the symmetry half of that hypothesis at the annealed block — unconditionally, since the sample response is symmetric at every field and the annealed block is its entrywise expectation — and then assembles the printed form of Θ_m and of the reference aspect ratio Π under e.coarse.ellipticity alone: positive definiteness of the annealed block is a consequence of that assumption, and positive definiteness of the reference block is one of its fields.

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_annealedBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : IsSymmetricBlockMat (annealedBlock P U)

The annealed block is a symmetric doubled matrix, at every law and every cell. Symmetry of the sample response is pointwise in the field, and the annealed block is the entrywise expectation, so no integrability is needed.

theorem HCPolySupport.HighContrast.annealedContrast_eq_sInf_conj {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {m : ℤ} (hpos : Book.Ch02.BlockPosDef (annealedBlock P (centeredCube d m))) : annealedContrast P m = sInf ((fun (h : Mat d) => specBound (matSqrt (annealedBlock P (centeredCube d m)).lowerRight * skewCorrectedForm (annealedBlock P (centeredCube d m)) h * matSqrt (annealedBlock P (centeredCube d m)).lowerRight)) '' {h : Mat d | IsSkewMat h})

The annealed contrast in printed form. On a positive definite annealed block, Θ_m is the infimum over skew h of the conjugated norms |σ_bar_*^{-1/2} (σ_bar + (k_bar - h)ᵗ σ_bar_*⁻¹ (k_bar - h)) σ_bar_*^{-1/2}| of e.Theta.m, the conjugating matrix being the positive semidefinite square root of the lower-right block σ_bar_*⁻¹.

The printed objects of the frozen conclusion

theorem HCPolySupport.HighContrast.annealedContrast_eq_sInf_conj_of_coarseEllipticityDagger {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) : annealedContrast P m = sInf ((fun (h : Mat d) => specBound (matSqrt (annealedBlock P (centeredCube d m)).lowerRight * skewCorrectedForm (annealedBlock P (centeredCube d m)) h * matSqrt (annealedBlock P (centeredCube d m)).lowerRight)) '' {h : Mat d | IsSkewMat h})

Under e.coarse.ellipticity the annealed block is positive definite at every scale, so Θ_m is the infimum of the printed family with no further hypothesis.

theorem HCPolySupport.HighContrast.isLeast_norm_annealedContrast_of_coarseEllipticityDagger {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) : IsLeast ((fun (h : Mat d) => ‖matSqrt (annealedBlock P (centeredCube d m)).lowerRight * skewCorrectedForm (annealedBlock P (centeredCube d m)) h * matSqrt (annealedBlock P (centeredCube d m)).lowerRight‖) '' {h : Mat d | IsSkewMat h}) (annealedContrast P m)

Θ_m is exactly the printed object. Under e.coarse.ellipticity the annealed contrast of the frozen conclusion is the least value of |σ_bar_*^{-1/2} (σ_bar + (k_bar - h)ᵗ σ_bar_*⁻¹ (k_bar - h)) σ_bar_*^{-1/2}| over the skew matrices, the bars being the spectral norm: the minimum written at e.Theta.m, attained, with no infimum reading left over.

theorem HCPolySupport.HighContrast.isLeast_norm_bigLambdaRef_of_coarseEllipticityDagger {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : IsLeast ((fun (h : Mat d) => ‖skewCorrectedForm E h‖) '' {h : Mat d | IsSkewMat h}) (bigLambdaRef E)

Λ_0 is exactly the printed object under e.coarse.ellipticity: the reference block of the assumption is symmetric and positive definite, which is all the printed minimum needs.

theorem HCPolySupport.HighContrast.exists_isSkewMat_aspectRatio_eq_norm_of_coarseEllipticityDagger {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : ∃ (h : Mat d), IsSkewMat h ∧ aspectRatio E = ‖skewCorrectedForm E h‖ / ‖E.lowerRight‖⁻¹

Π is exactly the printed aspect ratio under e.coarse.ellipticity: the quotient Λ_0 / λ_0 of e.reference.aspect.ratio, the numerator a minimum of spectral norms realized at a skew matrix.