High-contrast homogenization: Entry.Response.Core.SkewShearCongruence

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

The skew-shear congruence of the coarse block

This file develops the skew-shear congruence that removes the skew part of the coarse block matrix in the proof of adapted_response_core: it shows the shear conjugation subtracts exactly the skew component, expresses the sheared block-matrix-vector product and block energy density in terms of the unsheared ones, and proves the shear preserves the admissible class of Radon measures. It also proves the helper facts the response-imbalance comparison needs: monotonicity of the canonical imbalance, the index bound j* < s at a raw sample, and the elementary inequalities relating the determinant ratio to the scale factor. The congruence serves the response transfer p.response.transfer; the imbalance helpers serve the comparison e.response.imbalance.comparison.

The skew-shear congruence and response-imbalance helpers

This file develops the skew-shear congruence for the coarse block matrix in the proof of adapted_response_core, together with the admissible-class lemmas it rests on and the helper lemmas for the response-imbalance comparison.

The skew-shear congruence

The identity coarseBlockMatrix U (fun x => a x - g) = blockCongr (1, 0, g, 1) (coarseBlockMatrix U a) for a constant skew matrix g (p.response.transfer), together with the admissible-class lemmas it rests on. It is the mathematical content of annealedBlockOf_respCoeffMinus_eq, proved here from the CoarseGraining primitives.

def HCPolySupport.HighContrast.Multiscale.shearStateFluxAdd {d : ℕ} (g : Mat d) (X : BlockState d) : BlockState d

Keep the potential of a block state and add g times that potential to its flux.

Equations

• HCPolySupport.HighContrast.Multiscale.shearStateFluxAdd g X = { potential := X.potential, flux := fun (x : HCPolySupport.Vec d) => X.flux x + HCPolySupport.matVecMul g (X.potential x) }

def HCPolySupport.HighContrast.Multiscale.shearLoad {d : ℕ} (g : Mat d) (P : BlockVec d) : BlockVec d

Shear a block load by keeping its first component and adding g times that component to the second.

Equations

• HCPolySupport.HighContrast.Multiscale.shearLoad g P = (P.1, P.2 + HCPolySupport.matVecMul g P.1)

theorem HCPolySupport.HighContrast.Multiscale.Mu_sub_skew_shearLoad {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (g : Mat d) (hg : matTranspose g = -g) (P : BlockVec d) : (Mu U P fun (x : Vec d) => a x - g) = Mu U (shearLoad g P) a

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_blockCongr {d : ℕ} (G A : BlockMat d) (P : BlockVec d) : blockVecDot P (blockMatVecMul (blockCongr G A) P) = blockVecDot (blockMatVecMul G P) (blockMatVecMul A (blockMatVecMul G P))

theorem HCPolySupport.HighContrast.Multiscale.blockMatVecMul_shear_eq_shearLoad {d : ℕ} (g : Mat d) (P : BlockVec d) : blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } P = shearLoad g P

theorem HCPolySupport.HighContrast.Multiscale.isSymmetricBlockMat_blockCongr {d : ℕ} (G : BlockMat d) {A : BlockMat d} (hA : IsSymmetricBlockMat A) : IsSymmetricBlockMat (blockCongr G A)

theorem HCPolySupport.HighContrast.Multiscale.coarseBlockMatrix_sub_skew_eq_blockCongr {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {g : Mat d} (hg : matTranspose g = -g) (hquad : HasQuadraticMu U a) : (coarseBlockMatrix U fun (x : Vec d) => a x - g) = blockCongr { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } (coarseBlockMatrix U a)

Helpers for the response-imbalance comparison

These private lemmas supply the monotonicity of the canonical imbalance, the determinant and eigenvalue estimates for positive-definite matrices, and the block positive-definiteness criterion used in e.response.imbalance.comparison.

theorem HCPolySupport.HighContrast.Multiscale.jStar_lt_s_of_raw (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (ε σ Cglob Cprof Csrc Bresp : ℝ) (hε : ε ∈ Set.Ioc 0 S.eps0) (hσ : σ ∈ Set.Ioc 0 ε) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (raw : RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t) : ↑jStar < s

With the two premises ε ∈ (0, S.eps0] and σ ∈ (0, ε] that the paper's Step 2 uses, the raw output gives j_* < s, which is what Annealed.adaptedMean_antitone needs for E_t ≤ E_s. Without them S.one_le_B0 is unavailable, B may be negative and raw.hs_lo is vacuous.

theorem HCPolySupport.HighContrast.Multiscale.canonicalImbalance_mono {d : ℕ} {A Bm : BlockMat d} (hAs : IsSymmetricBlockMat A) (hA : Book.Ch02.BlockPosDef A) (hBs : IsSymmetricBlockMat Bm) (hB : Book.Ch02.BlockPosDef Bm) (hAB : toFullBlockMat A ≤ toFullBlockMat Bm) : canonicalImbalance A ≤ canonicalImbalance Bm

The canonical imbalance is monotone for the Loewner order: A ≤ B implies 𝔡(A) ≤ 𝔡(B).

This is the Lean content of the middle inequality κ_t ≤ κ_s of e.response.imbalance.comparison: 𝔡(B) ≤ c unpacks to B ≤ c·𝐑B⁻¹𝐑 (le_of_imbalance_le), inverse antitonicity turns A ≤ B into 𝐑B⁻¹𝐑 ≤ 𝐑A⁻¹𝐑, and imbalance_le_of_le packs A ≤ c·𝐑A⁻¹𝐑 back up.

theorem HCPolySupport.HighContrast.Multiscale.one_le_canonicalImbalance {d : ℕ} (hd : 2 ≤ d) {A : BlockMat d} (hAs : IsSymmetricBlockMat A) (hA : Book.Ch02.BlockPosDef A) (hswap : toFullBlockMat (blockSwap d) * (toFullBlockMat A)⁻¹ * toFullBlockMat (blockSwap d) ≤ toFullBlockMat A) : 1 ≤ canonicalImbalance A

1 ≤ 𝔡(A) whenever the primal-adjoint order 𝐑A⁻¹𝐑 ≤ A holds (e.matrix.annealed.sharp.order, quoted at e.response.imbalance.comparison). This is the first inequality of e.response.imbalance.comparison.

theorem HCPolySupport.HighContrast.Multiscale.le_det_smul_one_of_one_le {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℝ} (hX : X.PosDef) (h1 : 1 ≤ X) : X ≤ X.det • 1

X ≤ X.det • 1 whenever X is positive-definite and 1 ≤ X: each eigenvalue of X is at most the product of all of them once every eigenvalue is ≥ 1.

theorem HCPolySupport.HighContrast.Multiscale.blockPosDef_of_full {d : ℕ} {A : BlockMat d} (hA : Matrix.PosDef (toFullBlockMat A)) : Book.Ch02.BlockPosDef A

A doubled block whose flattening is positive definite is block positive definite. The converse of posDef_toFullBlockMat, needed to feed Annealed.adaptedMean_posDef into the imbalance helpers (e.response.imbalance.comparison).

theorem HCPolySupport.HighContrast.Multiscale.le_detRatio_smul_of_le {n : Type u_1} [Fintype n] [DecidableEq n] {A Bm : Matrix n n ℝ} (hA : A.PosDef) (hB : Bm.PosDef) (hAB : A ≤ Bm) : 1 ≤ Bm.det / A.det ∧ Bm ≤ (Bm.det / A.det) • A

The determinant-ratio comparison of p.response.transfer: for positive definite A ≤ B one has 1 ≤ det B / det A and B ≤ (det B / det A) • A.

This is the step "bounding each eigenvalue of E_t^{-1/2} E_s E_t^{-1/2} by their product" (e.response.imbalance.comparison): congruating A ≤ B by A^{-1/2} produces X = A^{-1/2} B A^{-1/2} with 1 ≤ X and det X = det B / det A, and one_le_det_of_one_le / le_det_smul_one_of_one_le apply to X.