High-contrast homogenization: Provider.Quenched.SmallContrastWeakValue #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The weak value #
The weak-cap majorant, evaluated at the calibrated loads, is uniform over
unit directions: every load-dependent factor is a quadratic of the inflated
reference or of the recentered terminal mean at the load pair, and these are
bounded through the carried comparability and the smallness pack by the
absolute constants of the calibrated load quadratics. With the per-scale
variance carriers and mean drops bounded by supplied real values, both weak
quantities are at most ofReal of one explicit real weak value.
theorem
HCPolySupport.HighContrast.Quenched.calibrated_weak_loads
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q0 : Mat d}
(hq0 : Matrix.PosDef q0)
(t : ℤ)
(hint : HasFiniteAdaptedMean P q0 t)
{S0 SStar0 K0 : Mat d}
(hS0 : Matrix.PosDef S0)
(hStar0 : Matrix.PosDef SStar0)
(hform : toFullBlockMat (adaptedMean P q0 t) = schurBlock S0 SStar0 K0)
{eps : ℝ}
(hpos : 0 < eps)
(heps1 : eps ≤ 1)
(htr : ↑d * (schurHattedContrast S0 SStar0 - 1) ≤ eps)
{E F2 : BlockMat d}
{cF : ℝ}
(hcF0 : 0 ≤ cF)
(hF2eq : F2 = blockScale cF E)
(hF2pd : Book.Ch02.BlockPosDef F2)
{kap : ℝ}
(hkap0 : 0 ≤ kap)
(hcomp :
∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P q0 t) X))
(e : Vec d)
(he : e ⬝ᵥ e = 1)
:
Response.diagonalWeakLoadMinus (Response.skewBlockCongr (Response.responseSkew K0) F2)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0) SStar0)).mulVec
e) ≤ √(cF * kap * 7) ∧ Response.profileEnergyLoad
(Response.diagonalWeakLoadMinus F2
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e - matVecMul (Response.responseSkew K0)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)))
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e - matVecMul (Response.responseSkew K0)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)) ≤ √(cF * kap * 7 + 1) ∧ Response.diagonalWeakLoadMinus (Response.skewBlockCongr (Response.responseSkew K0) (adaptedMean P q0 t))
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e) ≤ √7 ∧ Response.diagonalWeakLoadPlus (Response.skewBlockCongr (Response.responseSkew K0) F2)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e) ≤ √(cF * kap * 7) ∧ Response.profileEnergyLoad
(Response.diagonalWeakLoadPlus F2
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e + matVecMul (Response.responseSkew K0)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)))
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e + matVecMul (Response.responseSkew K0)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)) ≤ √(cF * kap * 7 + 1) ∧ Response.diagonalWeakLoadPlus (Response.skewBlockCongr (Response.responseSkew K0) (adaptedMean P q0 t))
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)⁻¹).mulVec
e)
((matSqrt
(matGeomMean (S0 + Response.responseSymmetric K0 * SStar0⁻¹ * Response.responseSymmetric K0)
SStar0)).mulVec
e) ≤ √7
The six calibrated weak-load bounds.