Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.MagicIdentities.MuOrdering.UpperLeftAverage

Coarse-graining support: Support.CoarseGraining.MagicIdentities.MuOrdering.UpperLeftAverage #

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

Upper-left averaged matrix bounds #

This file upgrades the scalar quadratic upper-left estimate b(U; a) ≤ average(symmPart(a) + k(a)ᵀ symmPart(a)⁻¹ k(a)) to an honest matrix-order theorem.

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

Entrywise volume-average of the pointwise upper-left block coefficient.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.vecDot_matVecMul_averagedSymmPartPlusCorrection_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (p : Vec d) :
    vecDot p (matVecMul (averagedSymmPartPlusCorrection U a) p) = volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (symmPart (a x) + matTranspose (skewPart (a x)) * (symmPart (a x))⁻¹ * skewPart (a x)) p)
    source
    theorem HCPolySupport.bCoarse_le_averagedSymmPartPlusCorrection_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)) {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 (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) (averagedSymmPartPlusCorrection U a)

    Note-facing upper-left matrix-order bound b(U; a) ≤ average(symmPart(a) + k(a)ᵀ symmPart(a)⁻¹ k(a)).

    source
    theorem HCPolySupport.bCoarse_le_averagedSymmPartPlusCorrection_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)) {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 (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) (averagedSymmPartPlusCorrection U a)