High-contrast homogenization: Entry.CG.Proofs.AdaptedDomainRecovery

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

Convex-domain recovery and affine open cubes

On every bounded open convex domain with positive real volume, the canonical potential/solenoidal recovery data realizes the Mu infimum. This module proves that identification from CG's Hilbert minimizer and representative realization, then obtains the full coarse quadratic characterization and mixed response formula, which serve the response transfer p.response.transfer. Strict positivity uses pointwise ellipticity and the zero mean of both corrections.

The affine open-cube theorems discharge geometry and volume assumptions for every invertible matrix, integer scale, and real translation. All imports and declarations stay on CG's carriers. The sigma-matrix recovery package is not assumed: the direct mixed response/Mu route supplies the needed characterization. Their adapted-cell instances serve the fixed-geometry recurrence p.fixed.geometry.parent.child.recurrence.

theorem HCPolySupport.HighContrast.CG.exists_recoveryData_of_mu_eq_muCandidate_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} {lam Lam : ℝ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : ∃ (R : PotentialSolenoidalL2RecoveryData U), ∀ (P : BlockVec d), Mu U P a = (R.toMuHilbertRealization (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)).muCandidate P

On any bounded open convex domain, the canonical closure-based recovery package realizes the Hilbert minimizer value muCandidate.

theorem HCPolySupport.HighContrast.CG.exists_recovery_compatibility_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} {lam Lam : ℝ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : ∃ (R : PotentialSolenoidalL2RecoveryData U), Nonempty (R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol))

The recovery compatibility package on any bounded open convex domain.

theorem HCPolySupport.HighContrast.CG.isCoarseBlockMatrix_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} {lam Lam : ℝ} {a : CoeffField d} (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : IsCoarseBlockMatrix U a (coarseBlockMatrix U a)

The canonical coarse block matrix is characterized by the variational quadratic identity on any bounded open convex domain.

theorem HCPolySupport.HighContrast.CG.responseJ_eq_block_quadratic_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} {lam Lam : ℝ} {a : CoeffField d} (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (p r : Vec d) : ResponseJ U p r a = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (coarseBlockMatrix U a) (-p, r)) - vecDot p r

Mixed scalar response as the canonical coarse-block quadratic expression on any bounded open convex domain.

theorem HCPolySupport.HighContrast.CG.blockPosDef_coarseBlockMatrix_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} {lam Lam : ℝ} {a : CoeffField d} (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : Book.Ch02.BlockPosDef (coarseBlockMatrix U a)

Strict positivity follows from an attained energy minimum. Pointwise ellipticity makes zero energy force the minimizer to vanish a.e.; the zero-mean corrections then force its prescribed block vector to vanish. No sigma-matrix recovery premise is needed.

theorem HCPolySupport.HighContrast.CG.isOpenBoundedConvexDomain_affine_openCube {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) : IsOpenBoundedConvexDomain (translateSet y (matVecMul q '' openCubeSet (originCube d j)))

Invertible affine images of open triadic cubes are bounded open convex domains.

theorem HCPolySupport.HighContrast.CG.volume_affine_openCube_toReal_pos {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) : 0 < (MeasureTheory.volume (translateSet y (matVecMul q '' openCubeSet (originCube d j)))).toReal

Every invertible affine open cube has positive finite real volume, for every integer scale.

theorem HCPolySupport.HighContrast.CG.responseJ_congr_of_ae_eq {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (hab : a =ᵐ[MeasureTheory.volume.restrict U] b) (p r : Vec d) : ResponseJ U p r a = ResponseJ U p r b

The scalar response depends only on the coefficient a.e. class on its domain.

theorem HCPolySupport.HighContrast.CG.isCoarseBlockMatrix_affine_openCube {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a) : IsCoarseBlockMatrix (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a (coarseBlockMatrix (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a)

The variational characterization on an arbitrary invertible affine open cube.

theorem HCPolySupport.HighContrast.CG.blockPosDef_coarseBlockMatrix_affine_openCube {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a) : Book.Ch02.BlockPosDef (coarseBlockMatrix (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a)

Strict positivity on an arbitrary invertible affine open cube.

theorem HCPolySupport.HighContrast.CG.responseJ_eq_block_quadratic_affine_openCube {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a) (p r : Vec d) : ResponseJ (translateSet y (matVecMul q '' openCubeSet (originCube d j))) p r a = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (coarseBlockMatrix (translateSet y (matVecMul q '' openCubeSet (originCube d j))) a) (-p, r)) - vecDot p r

The full mixed response identity on an arbitrary invertible affine open cube.