High-contrast homogenization: Provider.Quenched.SmallContrastCalibrationAlgebra

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

Calibration algebra for the centering estimate

The response metric is the geometric mean m = b # S₊ of the corrected block and the lower Schur datum. This file records the finite-dimensional facts the centering estimate consumes: a positive semidefinite matrix is dominated by its trace, the calibrated S₊-energies of the two loads are the quadratics of the normalized corrected block B = m^{-1/2} b m^{-1/2} and of its inverse, and B dominates the identity.

Dot-product transport

theorem HCPolySupport.HighContrast.Quenched.mulVec_dotProduct_symm {d : ℕ} {C : Mat d} (hC : Matrix.conjTranspose C = C) (x w : Vec d) : Matrix.mulVec C x ⬝ᵥ w = x ⬝ᵥ Matrix.mulVec C w

Transport of a symmetric factor across the dot product.

theorem HCPolySupport.HighContrast.Quenched.dotProduct_self_nonneg' {d : ℕ} (x : Vec d) : 0 ≤ x ⬝ᵥ x

The dot square of a vector is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.dotProduct_sq_le {d : ℕ} (x y : Vec d) : (x ⬝ᵥ y) ^ 2 ≤ x ⬝ᵥ x * y ⬝ᵥ y

Cauchy–Schwarz for the dot product.

A positive semidefinite matrix is dominated by its trace

theorem HCPolySupport.HighContrast.Quenched.vecMulVec_mulVec_self {d : ℕ} (x y : Vec d) : (Matrix.vecMulVec x x).mulVec y = (x ⬝ᵥ y) • x

The rank-one square applied to a vector.

theorem HCPolySupport.HighContrast.Quenched.posSemidef_vecMulVec_self {d : ℕ} (x : Vec d) : (Matrix.vecMulVec x x).PosSemidef

The rank-one square is positive semidefinite.

theorem HCPolySupport.HighContrast.Quenched.vecMulVec_le_smul_one {d : ℕ} (x : Vec d) : Matrix.vecMulVec x x ≤ (x ⬝ᵥ x) • 1

The rank-one square is dominated by the vector energy.

theorem HCPolySupport.HighContrast.Quenched.trace_mul_vecMulVec {d : ℕ} (T : Mat d) (x : Vec d) : (T * Matrix.vecMulVec x x).trace = x ⬝ᵥ Matrix.mulVec T x

The trace against a rank-one square is the quadratic form.

theorem HCPolySupport.HighContrast.Quenched.psd_quad_le_trace {d : ℕ} {T : Mat d} (hT : Matrix.PosSemidef T) (x : Vec d) : x ⬝ᵥ Matrix.mulVec T x ≤ Matrix.trace T * x ⬝ᵥ x

A positive semidefinite quadratic form is dominated by the trace.

theorem HCPolySupport.HighContrast.Quenched.psd_le_smul_one {d : ℕ} {T : Mat d} (hT : Matrix.PosSemidef T) {c : ℝ} (hc : ∀ (x : Vec d), x ⬝ᵥ Matrix.mulVec T x ≤ c * x ⬝ᵥ x) : T ≤ c • 1

A positive semidefinite matrix is dominated by any scalar bound on its quadratic form.

theorem HCPolySupport.HighContrast.Quenched.psd_sq_le_smul {d : ℕ} {T : Mat d} (hT : Matrix.PosSemidef T) {c : ℝ} (hc : T ≤ c • 1) : T * T ≤ c • T

The square of a positive semidefinite matrix below c·1 is below c times the matrix.

The normalized corrected block

noncomputable def HCPolySupport.HighContrast.Quenched.calibrationB {d : ℕ} (b SStar : Mat d) : Mat d

The normalized corrected block B = m^{-1/2} b m^{-1/2} at the metric m = b # S₊.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.calibrationB_posDef {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) : Matrix.PosDef (calibrationB b SStar)

theorem HCPolySupport.HighContrast.Quenched.calibrationB_inv {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) : (calibrationB b SStar)⁻¹ = matSqrt (matGeomMean b SStar) * b⁻¹ * matSqrt (matGeomMean b SStar)

The inverse of the normalized corrected block.

theorem HCPolySupport.HighContrast.Quenched.metric_conj_sStar {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) : matSqrt (matGeomMean b SStar)⁻¹ * SStar * matSqrt (matGeomMean b SStar)⁻¹ = (calibrationB b SStar)⁻¹

The Riccati conjugation: the calibrated S₊-energy of the p-load is the inverse normalized block.

theorem HCPolySupport.HighContrast.Quenched.metric_conj_sStarInv {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) : matSqrt (matGeomMean b SStar) * SStar⁻¹ * matSqrt (matGeomMean b SStar) = calibrationB b SStar

The mirrored Riccati conjugation: the calibrated S₊⁻¹-energy of the r-load is the normalized block itself.

theorem HCPolySupport.HighContrast.Quenched.sStar_le_metric {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (hbStar : SStar ≤ b) : SStar ≤ matGeomMean b SStar

The metric lies above the lower Schur datum.

theorem HCPolySupport.HighContrast.Quenched.metric_le_b {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (hbStar : SStar ≤ b) : matGeomMean b SStar ≤ b

The metric lies below the corrected block.

theorem HCPolySupport.HighContrast.Quenched.one_le_calibrationB {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (hbStar : SStar ≤ b) : 1 ≤ calibrationB b SStar

The normalized corrected block dominates the identity.

theorem HCPolySupport.HighContrast.Quenched.calibrationB_inv_le_one {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (hbStar : SStar ≤ b) : (calibrationB b SStar)⁻¹ ≤ 1

The inverse normalized corrected block is below the identity.

Calibrated loads

theorem HCPolySupport.HighContrast.Quenched.calibration_pair {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (e : Vec d) : (matSqrt (matGeomMean b SStar)⁻¹).mulVec e ⬝ᵥ (matSqrt (matGeomMean b SStar)).mulVec e = e ⬝ᵥ e

The calibrated loads pair to the unit.

theorem HCPolySupport.HighContrast.Quenched.calibration_energy_p {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (e : Vec d) : (matSqrt (matGeomMean b SStar)⁻¹).mulVec e ⬝ᵥ Matrix.mulVec SStar ((matSqrt (matGeomMean b SStar)⁻¹).mulVec e) = e ⬝ᵥ (calibrationB b SStar)⁻¹.mulVec e

The S₊-energy of the p-load is the B⁻¹-quadratic.

theorem HCPolySupport.HighContrast.Quenched.calibration_energy_r {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) (e : Vec d) : (matSqrt (matGeomMean b SStar)).mulVec e ⬝ᵥ SStar⁻¹.mulVec ((matSqrt (matGeomMean b SStar)).mulVec e) = e ⬝ᵥ Matrix.mulVec (calibrationB b SStar) e

The S₊⁻¹-energy of the r-load is the B-quadratic.

Square-root conjugations and metric Cauchy–Schwarz

theorem HCPolySupport.HighContrast.Quenched.matSqrt_inv_conj_self {d : ℕ} {A : Mat d} (hA : Matrix.PosDef A) : matSqrt A⁻¹ * A * matSqrt A⁻¹ = 1

The inverse root conjugation of a positive matrix is the identity.

theorem HCPolySupport.HighContrast.Quenched.dotProduct_sq_le_quad_mul_quad {d : ℕ} {M : Mat d} (hM : Matrix.PosDef M) (x y : Vec d) : (x ⬝ᵥ y) ^ 2 ≤ x ⬝ᵥ Matrix.mulVec M x * y ⬝ᵥ M⁻¹.mulVec y

Cauchy–Schwarz in a positive metric.