High-contrast homogenization: Provider.Entry.ContrastBridge

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

The entry contrast against the Euclidean imbalance

The last display of the proof of t.polynomial.entry converts the imbalance of the Euclidean annealed block at the entry generation into the annealed contrast there,

Θ_m - 1 ≤ 3(𝔡(F_m) - 1),

with Θ_m the intrinsic annealed contrast of e.Theta.m and 𝔡 the canonical imbalance of e.scale.selection.canonical.metric, both read on F_m = 𝐀_bar(□_m).

Two things are proved.

Definedness. The printed argument obtains the finiteness and positive definiteness of F_m from the Euclidean mean comparison e.initial.source.bounds, which is available at generations at or above the source burn. Both are in fact consequences of e.coarse.ellipticity alone, at every generation: the coarse response of a centered cube is integrable and its expectation is positive definite, and the annealed primal-adjoint order then puts the block above its own sharp. The generation hypothesis is carried below for the shape of the entry argument and is not needed.

The comparison. The bridge itself is Θ ≤ 𝔡 on any symmetric positive doubled block — one factor of three stronger than the printed display, which is recovered from it because 𝔡 ≥ 1.

The printed route to the display passes through the uncorrected Schur ratio Θ_tilde = |σ_*^{-1/2} σ σ_*^{-1/2}|, in two steps: a factor-three comparison Θ - 1 ≤ 3(Θ_tilde - 1), and then Θ_tilde - 1 ≤ 𝔡 - 1 read off the sharp ordering. The second step's source, the lower block inequality of [Armstrong–Kuusi, Lemma 2.6, (2.82)], is false as printed: at Schur data σ_* = 1, σ = 9, k = 4 in one dimension the printed bounds are exceeded, both being linear in Θ_tilde - 1 where the extremal configurations grow quadratically. Neither step is used here.

The route taken instead is the intrinsic minimum itself. Θ minimizes the normalized skew-corrected Schur form over the skew matrices, so any skew matrix bounds it; the choice h = ½(k - kᵗ) leaves the symmetric coordinate r = ½(k + kᵗ) and the corrected form B = σ + rᵗσ_*⁻¹r, and the fourfold Schur bound of e.response.canonical.imbalance — the imbalance ordering F ≤ 𝔡 F^♯ read at the vector whose second Schur coordinate vanishes — gives σ + 4rᵗσ_*⁻¹r ≤ 𝔡 σ_*, hence B ≤ 𝔡 σ_*. So 𝔡 is admissible for the infimum defining Θ, which is exactly Θ ≤ 𝔡. The uncorrected ratio never appears.

There are no definitions in this file.

The bridge

theorem HCPolySupport.HighContrast.Entry.blockContrast_le_blockImbalance {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : blockContrast F ≤ blockImbalance F

The intrinsic contrast is below the canonical imbalance, Θ ≤ 𝔡, on every symmetric positive definite doubled block.

The skew matrix h = ½(k - kᵗ) corrects the Schur skew coordinate to its symmetric part r = ½(k + kᵗ), and the imbalance ordering F ≤ 𝔡 F^♯ of e.scale.selection.canonical.metric, read on the doubled coordinate whose second Schur component vanishes, bounds σ + rᵗσ_*⁻¹r by 𝔡 σ_*. That is an admissible Loewner scaling for the infimum defining the intrinsic contrast, so the infimum is at most 𝔡.

The Euclidean block at a generation of the entry argument

theorem HCPolySupport.HighContrast.Entry.blockSharp_annealedBlock_centeredCube_le {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 : ℤ) : BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d m))) (annealedBlock P (centeredCube d m))

The Euclidean annealed block dominates its own sharp under e.coarse.ellipticity. Integrability of the coarse response of a centered cube and positivity of its expectation are consequences of the assumption at every generation, and the annealed primal-adjoint order applies on the cube.

theorem HCPolySupport.HighContrast.Entry.one_le_blockImbalance_annealedBlock_centeredCube {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 : ℤ) : 1 ≤ blockImbalance (annealedBlock P (centeredCube d m))

The Euclidean imbalance is at least one under e.coarse.ellipticity: the determinant clause for the canonical metric on a block above its own sharp.

The entry conversion

theorem HCPolySupport.HighContrast.Entry.entry_contrast (d : ℕ) (hd : 2 ≤ d) (g : ℝ) (_hg : g ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (_hstat : IsStationaryLaw P) (_hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) (_hm : sourceBurn d (↑(initExpQ d g)) K ≤ m) : annealedContrast P m - 1 ≤ 3 * (blockImbalance (annealedBlock P (centeredCube d m)) - 1)

The entry contrast conversion of t.polynomial.entry: at every generation the annealed contrast of the centered cube is converted into the imbalance of the Euclidean annealed block there,

Θ_m - 1 ≤ 3(𝔡(F_m) - 1).

The comparison Θ_m ≤ 𝔡(F_m) is one factor of three stronger; the printed display follows because the imbalance is at least one. The source-burn hypothesis, which the printed definedness step consumes, is not needed: the definedness of F_m is available from e.coarse.ellipticity at every generation.