Coarse-graining support: Support.CoarseGraining.Symmetric.OpenBoundedConvex #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Symmetric response wrappers on open bounded convex domains #
The core symmetric response identities require the determinant guard
IsUnit sigmaStar.det. On open bounded convex domains, elliptic recovery data
supplies this guard from the usual deterministic hypotheses.
theorem
HCPolySupport.responseJ_eq_half_dot_sigmaCoarse_add_half_dot_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))
{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)
(p q : Vec d)
:
Open-bounded-convex wrapper for the symmetric split quadratic response formula.
theorem
HCPolySupport.responseJ_completedSquare_of_symmetricEllipticOnConvexDomain
{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)
(p q : Vec d)
:
Open-bounded-convex wrapper for the symmetric completed-square identity.
theorem
HCPolySupport.responseJ_sigmaStarCoarse_mul_eq_half_gap_of_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))
{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)
(p : Vec d)
:
ResponseJ U p (matVecMul (sigmaStarCoarse U a) p) a = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
Open-bounded-convex wrapper for the canonical symmetric gap identity at
q = sigmaStarCoarse p.