Coarse-graining support: Support.Internal.Ch02.MatrixExtraction #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Internal.Ch02.BookCh02.exists_recoveryData_of_mu_eq_muCandidate_of_isOpenBoundedConvexDomain
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain U)
{lam Lam : ℝ}
{a : CoeffField d}
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : 0 < (MeasureTheory.volume U).toReal)
:
∃ (R : PotentialSolenoidalL2RecoveryData U),
∀ (P : BlockVec d),
Mu U P a = (R.toMuHilbertRealization (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)).muCandidate P
On a bounded open convex domain, the canonical closure-based recovery data
realizes the Hilbert minimizer value muCandidate.
theorem
HCPolySupport.Internal.Ch02.BookCh02.exists_oldCanonicalMatrixData_of_isOpenBoundedConvexDomain
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain U)
{lam Lam : ℝ}
{a : CoeffField d}
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : 0 < (MeasureTheory.volume U).toReal)
:
∃ (R : PotentialSolenoidalL2RecoveryData U) (sigma0 : Mat d) (_ :
R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)),
IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a) ∧ IsSigmaStarInvCoarse U a (sigmaStarInvCoarse U a) ∧ IsSigmaStarCoarse U a (sigmaStarCoarse U a) ∧ IsKappaCoarse U a (sigmaStarCoarse U a) (kappaCoarse U a) ∧ IsSigmaCoarse U a sigma0 (sigmaStarCoarse U a) (kappaCoarse U a) ∧ IsSigmaCanonicalCoarse U a (sigmaCoarse U a)
Internal package of old coarse-matrix data, with all recovery and compatibility witnesses hidden behind bounded-open-convex domain hypotheses.
theorem
HCPolySupport.Internal.Ch02.BookCh02.canonicalResponseMatrixIdentities_of_isEllipticFieldOn
{d : ℕ}
[NeZero d]
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.canonicalResponseMatrixIdentities_of_neZero
{d : ℕ}
[NeZero d]
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.canonicalResponseMatrixIdentities
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
: