High-contrast homogenization: Provider.Quenched.AnnealedLimitBlock

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

The annealed limit block of the Euclidean cubes

The endgame display e.algebraic.block.decay compares the Euclidean annealed blocks 𝐀_bar(□_m) of e.Theta.m with a single deterministic limit block. This file constructs that limit and proves the half of the comparison that the coarse ellipticity assumption e.coarse.ellipticity already carries.

The annealed mean order of p.fixed.geometry.parent.child.recurrence, read on the identity grid, makes the doubled quadratic form of 𝐀_bar(□_n) nonincreasing along the nonnegative generations; positivity of the annealed block bounds it below. Each form therefore converges to its infimum, and the polarization identity of the doubled block turns the convergence of the three forms attached to a pair of doubled coordinates into convergence of the corresponding entry. The entrywise limits assemble into a symmetric doubled block whose form is exactly the infimum of the forms, so it lies Loewner-below every 𝐀_bar(□_m) with m ≥ 0.

The last section records the scalar dilation algebra of the doubled block that the two-sided comparison uses.

The forms of the Euclidean annealed blocks

noncomputable def HCPolySupport.HighContrast.Quenched.annealedForm {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (X : BlockVec d) (n : ℕ) : ℝ

The doubled quadratic form of the Euclidean annealed block, indexed by the nonnegative generations.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_annealedBlock_eq_annealedForm {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (n : ℕ) (α β : BlockCoord d) : blockMatEntry (annealedBlock P (centeredCube d ↑n)) α β = (annealedForm P (blockBasis α + blockBasis β) n - annealedForm P (blockBasis α) n - annealedForm P (blockBasis β) n) / 2

The entry of a Euclidean annealed block, recovered from the three forms of the polarization identity of the doubled block.

The limit block

noncomputable def HCPolySupport.HighContrast.Quenched.annealedLimitEntry {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (α β : BlockCoord d) : ℝ

The entries of the annealed limit block: the polarization combination of the infima of the three forms attached to a pair of doubled coordinates.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Quenched.annealedLimitBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) : BlockMat d

The annealed limit block 𝐀_bar: the doubled block assembled from the entrywise limits of the Euclidean annealed blocks.

Equations

• HCPolySupport.HighContrast.Quenched.annealedLimitBlock P = HCPolySupport.ofFullBlockMat (Matrix.of (HCPolySupport.HighContrast.Quenched.annealedLimitEntry P))

@[simp]

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_annealedLimitBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (α β : BlockCoord d) : blockMatEntry (annealedLimitBlock P) α β = annealedLimitEntry P α β

theorem HCPolySupport.HighContrast.Quenched.annealedLimitEntry_comm {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (α β : BlockCoord d) : annealedLimitEntry P α β = annealedLimitEntry P β α

theorem HCPolySupport.HighContrast.Quenched.isSymmetricBlockMat_annealedLimitBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) : IsSymmetricBlockMat (annealedLimitBlock P)

The annealed limit block is a symmetric doubled block.

Monotonicity and convergence under the coarse ellipticity assumption

theorem HCPolySupport.HighContrast.Quenched.annealedForm_antitone {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) (X : BlockVec d) : Antitone (annealedForm P X)

The forms of the Euclidean annealed blocks are nonincreasing. This is the annealed mean order of p.fixed.geometry.parent.child.recurrence at the identity grid, which holds from generation zero up.

theorem HCPolySupport.HighContrast.Quenched.annealedForm_nonneg {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) (X : BlockVec d) (n : ℕ) : 0 ≤ annealedForm P X n

The forms of the Euclidean annealed blocks are nonnegative.

theorem HCPolySupport.HighContrast.Quenched.bddBelow_range_annealedForm {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) (X : BlockVec d) : BddBelow (Set.range (annealedForm P X))

theorem HCPolySupport.HighContrast.Quenched.tendsto_annealedForm_ciInf {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) (X : BlockVec d) : Filter.Tendsto (annealedForm P X) Filter.atTop (nhds (⨅ (n : ℕ), annealedForm P X n))

Each form of the Euclidean annealed blocks converges to its infimum.

theorem HCPolySupport.HighContrast.Quenched.tendsto_blockMatEntry_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) (α β : BlockCoord d) : Filter.Tendsto (fun (n : ℕ) => blockMatEntry (annealedBlock P (centeredCube d ↑n)) α β) Filter.atTop (nhds (blockMatEntry (annealedLimitBlock P) α β))

The entries of the Euclidean annealed blocks converge to the entries of the annealed limit block.

theorem HCPolySupport.HighContrast.Quenched.tendsto_annealedForm_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) (X : BlockVec d) : Filter.Tendsto (annealedForm P X) Filter.atTop (nhds (blockVecDot X (blockMatVecMul (annealedLimitBlock P) X)))

The form of the annealed limit block is the limit of the forms of the Euclidean annealed blocks.

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_annealedLimitBlock_eq_ciInf {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) (X : BlockVec d) : blockVecDot X (blockMatVecMul (annealedLimitBlock P) X) = ⨅ (n : ℕ), annealedForm P X n

The form of the annealed limit block is the infimum of the forms of the Euclidean annealed blocks.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_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 (annealedLimitBlock P) (annealedBlock P (centeredCube d m))

The annealed limit block lies Loewner-below every Euclidean annealed block of a nonnegative generation.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_annealedLimitBlock_of_forall {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) {A : BlockMat d} (hA : ∀ (n : ℕ), BlockMatLoewnerLE A (annealedBlock P (centeredCube d ↑n))) : BlockMatLoewnerLE A (annealedLimitBlock P)

A doubled block below every Euclidean annealed block is below the limit. The limit is the greatest lower bound of the family in the Loewner order.

The scalar dilation algebra of the doubled block

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_blockMatVecMul_blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockScale c A) X) = c * blockVecDot X (blockMatVecMul A X)

The doubled quadratic form of a scalar dilation.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_of_le {d : ℕ} {c : ℝ} (hc : 0 ≤ c) {A B : BlockMat d} (h : BlockMatLoewnerLE A B) : BlockMatLoewnerLE (blockScale c A) (blockScale c B)

Scalar dilation by a nonnegative factor preserves the Loewner order.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_of_scalar_le {d : ℕ} {c c' : ℝ} (hcc : c ≤ c') {A : BlockMat d} (hA : Book.Ch02.BlockPosDef A) : BlockMatLoewnerLE (blockScale c A) (blockScale c' A)

Enlarging the scalar enlarges the dilation of a positive definite doubled block.