High-contrast homogenization: Provider.Quenched.AnnealedLimitSharpOrder

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

The sharp order around the annealed limit block

The annealed limit block of the Euclidean cubes is caught between a Euclidean annealed block and its primal-adjoint dual. The primal-adjoint involution reverses the Loewner order, so where the annealed blocks decrease along the generations their sharps increase, and the annealed primal-adjoint order keeps every sharp below its own block. Consequently

𝐀(□_m)^♯ ≼ 𝐀_bar ≼ 𝐀(□_m)

at every nonnegative generation, with 𝐀_bar the limit block. Two consequences are recorded.

Positivity. The sharp of a positive definite doubled block is positive definite, so the limit block is positive definite. This uses no quantitative decay of the annealed contrast.

The upper comparison. The canonical imbalance 𝔡 of e.scale.selection.canonical.metric satisfies F ≼ 𝔡(F) F^♯ by definition, so

𝐀_bar(□_m) ≼ 𝔡(𝐀_bar(□_m)) · 𝐀_bar.

The upper half of the endgame display e.algebraic.block.decay therefore follows from a scalar bound on the annealed imbalance alone.

The imbalance is an admissible dilation against the sharp

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_blockImbalance_blockSharp {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : BlockMatLoewnerLE F (blockScale (blockImbalance F) (blockSharp F))

A doubled block lies below its imbalance times its own sharp. This is the defining property of the canonical imbalance of e.scale.selection.canonical.metric, in the structural dialect.

The sharp order along the generations

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockSharp_annealedBlock {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {m : ℤ} (hm : 0 ≤ m) (n : ℕ) : BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d m))) (annealedBlock P (centeredCube d ↑n))

The sharp of a Euclidean annealed block lies below every Euclidean annealed block of a nonnegative generation. Above the given generation this is the order reversal of the primal-adjoint involution followed by the annealed primal-adjoint order; below it, the sharp order followed by the mean order of p.fixed.geometry.parent.child.recurrence.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockSharp_annealedLimitBlock {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {m : ℤ} (hm : 0 ≤ m) : BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d m))) (annealedLimitBlock P)

The sharp of a Euclidean annealed block lies below the annealed limit block.

theorem HCPolySupport.HighContrast.Quenched.blockPosDef_annealedLimitBlock {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) : Book.Ch02.BlockPosDef (annealedLimitBlock P)

The annealed limit block is positive definite. Its form dominates that of the sharp of a Euclidean annealed block, which is positive definite because that block is. No quantitative decay of the annealed contrast is used.

The upper comparison from a scalar imbalance bound

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_blockImbalance_annealedLimitBlock {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {m : ℤ} (hm : 0 ≤ m) : BlockMatLoewnerLE (annealedBlock P (centeredCube d m)) (blockScale (blockImbalance (annealedBlock P (centeredCube d m))) (annealedLimitBlock P))

The upper Loewner comparison against the annealed limit block, at the annealed imbalance. The block lies below its imbalance times its own sharp, and its sharp lies below the limit.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_annealedLimitBlock_of_blockImbalance_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {m : ℤ} (hm : 0 ≤ m) {c : ℝ} (hc : blockImbalance (annealedBlock P (centeredCube d m)) ≤ c) : BlockMatLoewnerLE (annealedBlock P (centeredCube d m)) (blockScale c (annealedLimitBlock P))

The upper half of the endgame block comparison follows from a scalar bound on the annealed imbalance.