Coarse-graining support: Support.CoarseGraining.Symmetric.Bracketing

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Dirichlet--Neumann bracketing for symmetric coefficient fields

This file records the symmetric specializations of the deterministic harmonic-mean and arithmetic-mean bounds for the canonical coarse matrices.

theorem HCPolySupport.averagedSymmPartInv_eq_volumeAverageMat_inv_of_isSymmetricCoeffField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) : averagedSymmPartInv U a = volumeAverageMat U fun (x : Vec d) => (a x)⁻¹

For symmetric coefficient fields, the averaged inverse symmetric part is the average of the pointwise inverse coefficient matrices.

theorem HCPolySupport.averagedSymmPartPlusCorrection_eq_volumeAverageMat_of_isSymmetricCoeffField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) : averagedSymmPartPlusCorrection U a = volumeAverageMat U a

For symmetric coefficient fields, the upper-left averaged correction is just the arithmetic average of the coefficient field.

theorem HCPolySupport.harmonicMeanCoeffField_le_sigmaStarCoarse_of_isSymmetricCoeffField {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (ha : IsSymmetricCoeffField a) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : MatLoewnerLE (volumeAverageMat U fun (x : Vec d) => (a x)⁻¹)⁻¹ (sigmaStarCoarse U a)

Symmetric harmonic-mean lower bound: (average_U a^{-1})^{-1} ≤ sigmaStarCoarse(U; a).

theorem HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_of_isSymmetricCoeffField_of_ellipticField {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (_ha : IsSymmetricCoeffField a) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) : MatLoewnerLE (sigmaStarCoarse U a) (sigmaCoarse U a)

The middle Dirichlet--Neumann ordering sigmaStarCoarse(U; a) ≤ sigmaCoarse(U; a), repackaged on the symmetric theorem surface.

theorem HCPolySupport.sigmaCoarse_le_volumeAverageMat_of_isSymmetricCoeffField_of_ellipticField {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (ha : IsSymmetricCoeffField a) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) : MatLoewnerLE (sigmaCoarse U a) (volumeAverageMat U a)

Symmetric arithmetic-mean upper bound: sigmaCoarse(U; a) ≤ average_U a.