High-contrast homogenization: Entry.Response.Core.LoadQuadraticSchur #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Schur bounds for the load quadratic forms #
This file proves the load-quadratic conjuncts of the response energy-and-defect estimate
e.response.energy.and.defect: it completes the load quadratic forms respEJ^∓ and respTau^∓
and proves they are nonnegative, then compares the recentred energies respEhatMinus/respEhatPlus
and the response mean across scales. The supporting algebra serves the response transfer
p.response.transfer: it proves the Schur identity for the block quadratic form under a block
swap, the Riccati exchange identity between the primal and swapped-conjugate quadratic forms, the
nonnegativity of the canonical imbalance, and the identity and bound for the sum of the load
quadratics respLsq^∓ used to compare scales.
The conjuncts #
theorem
HCPolySupport.HighContrast.Multiscale.respEJMinus_nonneg
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(jStar : ℕ)
(F : BlockMat d)
(t : ℤ)
(e : Vec d)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
:
First conjunct, unconditional (e.response.energy.and.defect).
theorem
HCPolySupport.HighContrast.Multiscale.respEJPlus_nonneg
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(jStar : ℕ)
(F : BlockMat d)
(t : ℤ)
(e : Vec d)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
:
Second conjunct, unconditional.
theorem
HCPolySupport.HighContrast.Multiscale.respEJMinus_eq_final
{d : ℕ}
[NeZero d]
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(jStar : ℕ)
(F : BlockMat d)
(t : ℤ)
(e : Vec d)
(he : vecDot e e = 1)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
(hM : Matrix.PosDef (respM (respMean P jStar F t)))
(hint : HasIntegrableCoarseBlock P (respCell jStar F t))
:
Third conjunct, from the raw output alone.
theorem
HCPolySupport.HighContrast.Multiscale.respEJPlus_eq_final
{d : ℕ}
[NeZero d]
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(jStar : ℕ)
(F : BlockMat d)
(t : ℤ)
(e : Vec d)
(he : vecDot e e = 1)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
(hM : Matrix.PosDef (respM (respMean P jStar F t)))
(hint : HasIntegrableCoarseBlock P (respCell jStar F t))
:
Fourth conjunct, from the raw output alone.
theorem
HCPolySupport.HighContrast.Multiscale.zero_le_respTauMinus_final
{d : ℕ}
[NeZero d]
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(jStar : ℕ)
(F : BlockMat d)
(s t : ℤ)
(e : Vec d)
(he : vecDot e e = 1)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
(hM : Matrix.PosDef (respM (respMean P jStar F t)))
(hord : BlockMatLoewnerLE (respMean P jStar F t) (respMean P jStar F s))
(hintT : HasIntegrableCoarseBlock P (respCell jStar F t))
(hintS : HasIntegrableCoarseBlock P (respCell jStar F s))
:
Seventh conjunct, from the raw output alone.
theorem
HCPolySupport.HighContrast.Multiscale.zero_le_respTauPlus_final
{d : ℕ}
[NeZero d]
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(jStar : ℕ)
(F : BlockMat d)
(s t : ℤ)
(e : Vec d)
(he : vecDot e e = 1)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
(hM : Matrix.PosDef (respM (respMean P jStar F t)))
(hord : BlockMatLoewnerLE (respMean P jStar F t) (respMean P jStar F s))
(hintT : HasIntegrableCoarseBlock P (respCell jStar F t))
(hintS : HasIntegrableCoarseBlock P (respCell jStar F s))
:
Eighth conjunct, from the raw output alone.
Part A: the Schur expansion of the block quadratic form #
Part B: b_t ≤ 𝔡(A) · σ_* #
Part B, conclusion: b_t ≤ 𝔡(A)·σ_* #
Part A2: the printed identity (L^-)^2 + (L^+)^2 = 4 p·b_t p #
Part C: from b_t ≤ 𝔡 σ_* to the energy bound #
Part C, conclusion #
theorem
HCPolySupport.HighContrast.Multiscale.ehatMinus_scale_cmp
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(jStar : ℕ)
(F : BlockMat d)
(s t : ℤ)
(X : BlockVec d)
(c : ℝ)
(hcmp :
∀ (Y : BlockVec d),
blockVecDot Y (blockMatVecMul (respMean P jStar F s) Y) ≤ c * blockVecDot Y (blockMatVecMul (respMean P jStar F t) Y))
:
blockVecDot X (blockMatVecMul (respEhatMinus P jStar F s) X) ≤ c * blockVecDot X (blockMatVecMul (respEhatMinus P jStar F t) X)
theorem
HCPolySupport.HighContrast.Multiscale.ehatPlus_scale_cmp
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(jStar : ℕ)
(F : BlockMat d)
(s t : ℤ)
(X : BlockVec d)
(c : ℝ)
(hcmp :
∀ (Y : BlockVec d),
blockVecDot Y (blockMatVecMul (respMean P jStar F s) Y) ≤ c * blockVecDot Y (blockMatVecMul (respMean P jStar F t) Y))
:
blockVecDot X (blockMatVecMul (respEhatPlus P jStar F s) X) ≤ c * blockVecDot X (blockMatVecMul (respEhatPlus P jStar F t) X)
theorem
HCPolySupport.HighContrast.Multiscale.respMean_scale_cmp
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(jStar : ℕ)
(F : BlockMat d)
(s t : ℤ)
(c : ℝ)
(hfull : toFullBlockMat (respMean P jStar F s) ≤ c • toFullBlockMat (respMean P jStar F t))
(Y : BlockVec d)
:
blockVecDot Y (blockMatVecMul (respMean P jStar F s) Y) ≤ c * blockVecDot Y (blockMatVecMul (respMean P jStar F t) Y)
The scale comparison E_s ≤ r E_t in quadratic-form shape.
Conjuncts 5, 6 (the energy bound) and 9, 10 (the defect bound) #
theorem
HCPolySupport.HighContrast.Multiscale.respEJ_le
{d : ℕ}
[NeZero d]
(hd : 2 ≤ d)
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(jStar : ℕ)
(F : BlockMat d)
(s t : ℤ)
(e : Vec d)
(he : vecDot e e = 1)
(hq : IsUnit (respGrid jStar F))
(hg : matTranspose (respg F) = -respg F)
(hsymm : IsSymmetricBlockMat (respMean P jStar F t))
(hposd : Book.Ch02.BlockPosDef (respMean P jStar F t))
(hint : HasIntegrableCoarseBlock P (respCell jStar F t))
(hkts : respKappa P jStar F t ≤ respKappa P jStar F s)
: