High-contrast homogenization: Provider.Persistence.EuclideanTransfer

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

The Euclidean transfer of the entry mean

The comparison between adapted and Euclidean cubes compares a Euclidean annealed block with an adapted mean up to an error measured in units of the reference block 𝐄. This file turns two such comparisons, read on the two distinct strict generation chains of the forward and of the reverse comparison, into the two-sided near-isometry e.response.transfer.block.comparison and a bound on the Euclidean imbalance after the transfer.

The mechanism is one congruence and one rearrangement. The congruence is the entry ratio Λ_t = |(E_t^q)^{-1/2}𝐄(E_t^q)^{-1/2}|, one of the normalization constants of the transfer: it is exactly the least scalar with 𝐄 ≤ Λ_t E_t^q, so an error c𝐄 whose congruenced size cΛ_t is below a tolerance η is an error below ηE_t^q. The forward comparison then reads as the upper Euclidean comparison.

The reverse comparison is one-sided in the wrong direction: it bounds the adapted mean at the auxiliary scale by the Euclidean block. The persistence clause at that scale turns it into a lower bound for the Euclidean block in terms of the entry mean, at the cost of the factor (1+δ_ad)^d, which is the lower Euclidean comparison. The tolerance conditions e.response.transfer.tolerances were chosen exactly so that the two one-sided bounds close up into the symmetric sandwich.

The last step is e.global.selection.metric.comparison at the sandwich: the Euclidean block is positive definite because it dominates a positive multiple of the entry mean — the Euclidean cube is not contained in the window, so this, and not the window estimate, is the route to its definedness.

The reference block measured against a positive block

theorem HCPolySupport.HighContrast.Persistence.toFullBlockMat_le_blockSize_smul {d : ℕ} {E F : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : toFullBlockMat E ≤ blockSize E F • toFullBlockMat F

The entry ratio is a Loewner bound. The scalar size blockSize E F = |F^{-1/2}EF^{-1/2}| is the least nonnegative t with E ≤ tF, so in particular it is one.

theorem HCPolySupport.HighContrast.Persistence.toFullBlockMat_blockScale_le_smul {d : ℕ} {E F : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {c eta : ℝ} (hc : 0 ≤ c) (hgap : c * blockSize E F ≤ eta) : toFullBlockMat (blockScale c E) ≤ eta • toFullBlockMat F

An error in units of the reference block, congruenced by a positive block. A dilation c𝐄 of the reference block whose congruenced size cΛ is below η is below ηF.

theorem HCPolySupport.HighContrast.Persistence.blockMatLoewnerLE_blockScale_mono {d : ℕ} {A B : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (hBpd : Book.Ch02.BlockPosDef B) {c₁ c₂ : ℝ} (hc : c₁ ≤ c₂) (h : BlockMatLoewnerLE A (blockScale c₁ B)) : BlockMatLoewnerLE A (blockScale c₂ B)

Enlarging the scalar of a dilation of a positive block preserves a Loewner upper bound.

The two absorptions

theorem HCPolySupport.HighContrast.Persistence.blockMatLoewnerLE_one_add {d : ℕ} {A B E : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (hE : IsSymmetricBlockMat E) {c eta : ℝ} (hsub : BlockMatLoewnerLE (blockSub A B) (blockScale c E)) (herr : toFullBlockMat (blockScale c E) ≤ eta • toFullBlockMat B) : BlockMatLoewnerLE A (blockScale (1 + eta) B)

The upper absorption, giving the upper Euclidean comparison: an adapter comparison A ≤ B + c𝐄 whose error is below ηB reads as A ≤ (1+η)B.

theorem HCPolySupport.HighContrast.Persistence.blockMatLoewnerLE_one_sub {d : ℕ} {A B C E : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (hC : IsSymmetricBlockMat C) (hE : IsSymmetricBlockMat E) (hBpd : Book.Ch02.BlockPosDef B) {c etaMinus ratio eta : ℝ} (hratio : 0 < ratio) (hsub : BlockMatLoewnerLE (blockSub C A) (blockScale c E)) (herr : toFullBlockMat (blockScale c E) ≤ etaMinus • toFullBlockMat B) (hpers : BlockMatLoewnerLE B (blockScale ratio C)) (htol : eta ≤ ratio⁻¹ - etaMinus) : BlockMatLoewnerLE (blockScale eta B) A

The lower absorption, giving the lower Euclidean comparison: an adapter comparison C ≤ A + c𝐄 in the wrong direction, whose error is below η₋B, becomes a lower bound for A once the persistence clause B ≤ ϱ C is available. Rearranging gives (ϱ^{-1} - η₋)B ≤ A, and the tolerance conditions e.response.transfer.tolerances weaken the scalar to the symmetric one.

The Euclidean imbalance

The Euclidean transfer