Documentation

LeanPool.HighContrastHomogenization.Entry.Response.Core.AdaptedDomainBridge

High-contrast homogenization: Entry.Response.Core.AdaptedDomainBridge #

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

Adapted cells as admissible domains #

This file shows that an adapted cell is an open, bounded, convex domain in the sense used throughout the argument, and develops the matrix algebra that lets the recentred coefficients be treated as elliptic fields on it. It proves that ellipticity of a field or a matrix survives adding or subtracting a skew correction, that the response correction is itself skew, and the accompanying facts about the Schur-swap skew congruence and the conversion between a block matrix and its full matrix form. Together these identify the adapted cell, equipped with the recentred coefficient, as a legitimate domain for the maximizer theory built on top of it. The module serves the response transfer p.response.transfer.

HC bridge I, part 1 of 4: adapted cells as Chapter-2 domains (B1) #

Section B1 only. See AnnealedBlockIdentity.lean for the closing docstring and AdaptedDomainBridge.lean for the re-export.

B1. Adapted cells are Chapter-2 domains. #

source
theorem HCPolySupport.HighContrast.Multiscale.adaptedCell_isOpenBoundedConvexDomain {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) :
IsOpenBoundedConvexDomain (adaptedCell q j)

U_t = q(centeredCube t) is an open bounded convex domain (p.response.transfer; old DomainBridge.lean). Route: HCPoly/Entry/Annealed/AdaptedDomainLocality.lean (isOpenBoundedConvexDomain_affine_openCube).

source
def HCPolySupport.HighContrast.Multiscale.adaptedDomain {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) :
Book.Ch02.Domain d

The adapted cell as a Chapter-2 domain.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Multiscale.isEllipticFieldOn_sub_skew {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {f : CoeffField d} (hf : IsEllipticFieldOn lam Lam U f) (g : Mat d) (hg : matTranspose g = -g) :
    IsEllipticFieldOn lam (2 * Lam + 2 * ‖g‖ ^ 2 / lam) U fun (x : Vec d) => f x - g

    A constant skew shift preserves ellipticity: the symmetric part of f - g is that of f, and |f - g| ≤ |f| + |g| (p.response.transfer, a_- = a - g). The ellipticity constant is 2 * Lam + 2 * ‖g‖ ^ 2 / lam, not Lam + ‖g‖; the latter is false because IsEllipticMatrix's A⁻¹ clause (Ambient/CoefficientField.lean) forces quadratic growth in ‖g‖.

    source
    theorem HCPolySupport.HighContrast.Multiscale.isEllipticFieldOn_transpose_add_skew {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {f : CoeffField d} (hf : IsEllipticFieldOn lam Lam U f) (g : Mat d) (hg : matTranspose g = -g) :
    IsEllipticFieldOn lam (2 * Lam + 2 * ‖g‖ ^ 2 / lam) U fun (x : Vec d) => matTranspose (f x) + g

    The transposed twin for a_+ = a^t + g (p.response.transfer). Same constant shape as above, 2 * Lam + 2 * ‖g‖ ^ 2 / lam; the constant Lam + ‖g‖ is false.

    Helpers for the response skewness #

    source
    theorem HCPolySupport.HighContrast.Multiscale.respg_isSkew {d : ℕ} (F : BlockMat d) :
    matTranspose (respg F) = -respg F

    respg F is skew (p.response.transfer: g is the skew Schur coefficient of M(F)).

    B2. Maximizer existence on adapted cells for the recentred coefficients. #

    CG provides ScalarCanonicalMaximizer.nonempty_of_isOpenBoundedConvexDomain (CoarseGraining/ResponseIdentities/Existence.lean) and HCPoly/Entry/Annealed/AdaptedDomainLocality.lean supplies lam Lam f with ⇑a.1 =ᵐ f. The sSup in respWeakEnergy is over a nonempty set.