Coarse-graining support: Support.CoarseGraining.MagicIdentities.MuOrdering.HarmonicMean

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

Harmonic-mean matrix bounds

This file upgrades the inverse-side scalar quadratic estimate σ_*^{-1} ≤ average(symmPart(a)^{-1}) to an honest matrix-order statement, and then inverts it to obtain the note-facing harmonic-mean lower bound for σ_*.

noncomputable def HCPolySupport.averagedSymmPartInv {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Mat d

Entrywise volume-average of the pointwise inverse symmetric part.

Equations

• HCPolySupport.averagedSymmPartInv U a = HCPolySupport.volumeAverageMat U fun (x : HCPolySupport.Vec d) => (HCPolySupport.symmPart (a x))⁻¹

theorem HCPolySupport.vecDot_matVecMul_averagedSymmPartInv_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (q : Vec d) : vecDot q (matVecMul (averagedSymmPartInv U a) q) = volumeAverage U fun (x : Vec d) => vecDot q (matVecMul (symmPart (a x))⁻¹ q)

theorem HCPolySupport.averagedSymmPartInv_posDef_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : Matrix.PosDef (averagedSymmPartInv U a)

theorem HCPolySupport.sigmaStarInvCoarse_le_averagedSymmPartInv_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)) : MatLoewnerLE (sigmaStarInvCoarse U a) (averagedSymmPartInv U a)

theorem HCPolySupport.sigmaStarInvCoarse_le_averagedSymmPartInv_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)) : MatLoewnerLE (sigmaStarInvCoarse U a) (averagedSymmPartInv U a)

theorem HCPolySupport.harmonicMeanSymmPart_le_sigmaStarCoarse_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)) : MatLoewnerLE (averagedSymmPartInv U a)⁻¹ (sigmaStarCoarse U a)

Note-facing harmonic-mean lower bound (average(symmPart(a)^{-1}))^{-1} ≤ σ_*(U; a).

theorem HCPolySupport.harmonicMeanSymmPart_le_sigmaStarCoarse_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)) : MatLoewnerLE (averagedSymmPartInv U a)⁻¹ (sigmaStarCoarse U a)