High-contrast homogenization: Provider.Persistence.AdaptedPersistence #

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

The adapted persistence of the annealed means #

The persistence of the adapted block above the response scale reads the adapted means of a rounded grid at every scale above the entry scale in both directions: the coarser mean lies below the entry mean, and the entry mean lies below (1+δ_ad)^d times the coarser one. The first half is the annealed mean order of p.fixed.geometry.parent.child.recurrence. The second is the determinant account.

Write Ξ(H) = det(H)^{1/d} for the determinant root of a doubled block. The determinant clause for the canonical metric reads, on a block that dominates its own sharp, as 1 ≤ det(H) ≤ 𝔡(H)^d, and the annealed primal-adjoint order makes every adapted mean of the tower dominate its own sharp. So the coarser mean has determinant at least one, and the entry mean has determinant at most the d-th power of its imbalance, which the adapted-imbalance hypothesis caps at 1+δ_ad. The determinant quotient of the ordered pair is therefore at most (1+δ_ad)^d, and e.global.selection.metric.loss turns a determinant quotient bounded by r^d into the Loewner comparison E ≤ r^d F for the pair it is read on.

The account is unconditional in the sense that it consumes only the finiteness of the entry mean: the finiteness of the coarser mean, which both halves need in order to denote, is supplied by the upward integrability of the companion file.

Two order facts about scalar dilations and the imbalance #

source

theorem HCPolySupport.HighContrast.Persistence.smul_le_smul_of_le_right {n : Type u_1} {A : Matrix n n ℝ} (hA : A.PosSemidef) {c₁ c₂ : ℝ} (h : c₁ ≤ c₂) :

c₁ • A ≤ c₂ • A

Dilation of a fixed positive semidefinite matrix is monotone in the scalar.

source

theorem HCPolySupport.HighContrast.Persistence.one_le_canonImbalance {d : ℕ} [Nonempty (Fin d)] {E : FullBlockMat d} (hE : Matrix.PosDef E) (hle : fullBlockSharp E ≤ E) :

1 ≤ canonImbalance E

The imbalance of a self-dominating positive block is at least one. The determinant clause for the canonical metric puts the determinant between one and the d-th power of the imbalance, so an imbalance below one would leave no room.

source

theorem HCPolySupport.HighContrast.Persistence.le_smul_of_det_div_le {d : ℕ} (hd : 2 ≤ d) {E F : FullBlockMat d} (hE : Matrix.PosDef E) (hF : Matrix.PosDef F) (hFE : F ≤ E) {c : ℝ} (hc : Matrix.det E / Matrix.det F ≤ c) :

E ≤ c • F

A determinant quotient bounded by c gives the Loewner comparison E ≤ cF. This is e.global.selection.metric.loss at the printed ratio, with the ratio's d-th power replaced by any upper bound for it.

The annealed sharp order at the adapted means #

source

theorem HCPolySupport.HighContrast.Persistence.blockSharp_adaptedMean_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {l : ℤ} {q : Mat d} [MeasureTheory.IsProbabilityMeasure P] (hq : IsRoundedGrid l q) (r : ℤ) (hfin : HasFiniteAdaptedMean P q r) :

BlockMatLoewnerLE (blockSharp (adaptedMean P q r)) (adaptedMean P q r)

The adapted mean dominates its own sharp. This is the annealed primal-adjoint order on the adapted cell, which is a nonempty bounded open convex domain as soon as the grid is positive definite.

source