Coarse-graining support: #
Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.SigmaStarInvAveraged
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
MuOrdering -- sigmaStarInvCoarse averaged-blockmatrix bounds #
sigmaStarInvCoarse_le_average_blockMatrixOfCoeff_lowerRight_… and the two
elliptic-bridge wrappers establishing the harmonic-mean-style upper bound
sigmaStarInvCoarse U a ≤ volumeAverage U (symmPart (a x))⁻¹ under
HodgeConverseCriterion / IsOpenBoundedConvexDomain.
theorem
HCPolySupport.sigmaStarInvCoarse_le_average_blockMatrixOfCoeff_lowerRight_of_mu_zero_right_eq_responseJ_zero
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{a : CoeffField d}
(hU : IsSobolevRegularDomain U)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(hMuResp : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a)
(q : Vec d)
:
vecDot q (matVecMul (sigmaStarInvCoarse U a) q) ≤ volumeAverage U fun (x : Vec d) => vecDot q (matVecMul (blockMatrixOfCoeff (a x)).lowerRight q)
theorem
HCPolySupport.sigmaStarInvCoarse_le_averaged_symmPart_inv_of_isEllipticFieldOn_of_hodgeConverseCriterion
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(R : PotentialSolenoidalL2RecoveryData U)
(hU : IsSobolevRegularDomain U)
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hHodge : HodgeConverseCriterion U)
(hvol : 0 < (MeasureTheory.volume U).toReal)
(compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol))
(q : Vec d)
:
vecDot q (matVecMul (sigmaStarInvCoarse U a) q) ≤ volumeAverage U fun (x : Vec d) => vecDot q (matVecMul (symmPart (a x))⁻¹ q)
theorem
HCPolySupport.sigmaStarInvCoarse_le_averaged_symmPart_inv_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(R : PotentialSolenoidalL2RecoveryData U)
(hConv : IsOpenBoundedConvexDomain U)
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : 0 < (MeasureTheory.volume U).toReal)
(compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol))
(q : Vec d)
:
vecDot q (matVecMul (sigmaStarInvCoarse U a) q) ≤ volumeAverage U fun (x : Vec d) => vecDot q (matVecMul (symmPart (a x))⁻¹ q)