High-contrast homogenization: Entry.Annealed.AnnealedBlockOrder #

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

Annealed Block Order #

The order-theoretic comparisons of the annealed block that serve p.fixed.geometry.parent.child.recurrence: Loewner monotonicity of the annealed mean under refinement, antitonicity of the annealed contrast in the scale, and the induced order of the full log-determinant.

Decreasing actual adapted means #

p.fixed.geometry.parent.child.recurrence: finite aligned subadditivity, integer stationarity, and genuine finite entrywise expectations. No averaging, positive-gap, or recurrence is used in this direction. Equality of generations is included.

source

theorem HCPolySupport.HighContrast.Annealed.coarseBlock_adapted_finite_partition {d : ℕ} [NeZero d] {ι : Type u_1} {s : Set ι} (hs : s.Finite) (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (qi : ι → Mat d) (hqi : ∀ i ∈ s, IsUnit (qi i)) (ji : ι → ℤ) (yi : ι → Vec d) (a : CoeffSpace d) :

have W := adaptedCellTranslate q j y; have U := fun (i : ι) => adaptedCellTranslate (qi i) (ji i) (yi i); (∀ i ∈ s, U i ⊆ W) → s.PairwiseDisjoint U → MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0 → BlockMatLoewnerLE (coarseBlock W a) (ofFullBlockMat (∑' (i : ↑s), ((MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (coarseBlock (U ↑i) a)))

A finite adapted partition satisfies the actual full block inequality.

source

theorem HCPolySupport.HighContrast.Annealed.coarseBlock_aligned_parent_le {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (h : ℕ) (a : CoeffSpace d) :

let s := {w : Fin d → ℤ | standardCellCenter j w ∈ centeredCube d (j + ↑h)}; have this := ⋯.fintype; BlockMatLoewnerLE (coarseBlock (adaptedCell q (j + ↑h)) a) (ofFullBlockMat (∑ w : ↑s, (3 ^ (d * h))⁻¹ • toFullBlockMat (coarseBlock (adaptedCellAtCenter q j ↑w) a)))

Pathwise aligned parent order with the literal finite equal-weight average.

source

theorem HCPolySupport.HighContrast.Annealed.annealedBlock_adaptedCellAtCenter {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (hj : ↑jStar ≤ j) (w : Fin d → ℤ) :

annealedBlock P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) j w) = adaptedMean P (Geometry.explicitRoundedGrid jStar m) j

Integer stationarity identifies each aligned child's actual annealed matrix.

source

theorem HCPolySupport.HighContrast.Annealed.adaptedMean_antitone (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j k : ℤ) (hj : ↑jStar ≤ j) (hjk : j ≤ k) :

BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar m) k) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)

Actual adapted annealed blocks decrease across every admissible pair, including j=k.

Monotonicity of the annealed contrast in the scale #

The Euclidean annealed contrast Θ_m of e.Theta.m is the intrinsic contrast of the annealed block of the centered cube □_m. Under the standing stationary law the annealed blocks of the centered cubes decrease in the doubled Loewner order as the scale grows, and the intrinsic contrast is monotone in that order. Hence Θ_m is nonincreasing in m beyond the rounding scale: a contrast bound at one scale is a contrast bound at every larger scale, which is the form in which t.polynomial.entry is consumed.

source

theorem HCPolySupport.HighContrast.Annealed.annealedContrast_antitone (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (j k : ℤ) (hj : ↑jStar ≤ j) (hjk : j ≤ k) :

annealedContrast P k ≤ annealedContrast P j

The annealed contrast is nonincreasing in the scale. Under the standing stationary law, Θ_k ≤ Θ_j whenever j ≤ k are at least the rounding scale: the annealed block of □_k lies below that of □_j in the doubled Loewner order, and the intrinsic contrast of e.Theta.m is monotone in that order.

Ordered means and the coefficient-one determinant loss #

p.fixed.geometry.parent.child.recurrence. Full doubled matrices are normalized without a commutation assumption. The determinant is the full 2d determinant, with no root.

source