Coarse-graining support: Support.CoarseGraining.MuRecovery.CorrectionSpaceSolenoidal

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

Mu correction-space recovery -- solenoidal / potential / responseSpace

upperImage isSolenoidalOn plus the lowerImage / upperImage memVectorL2, isPotential, and responseSpace membership theorems, both for the zero_right slice and in full form, under IsEllipticFieldOn.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_upperImage_isSolenoidalOn_zero_right {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : IsSolenoidalOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system (0, q)).eval x)).1

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_lowerImage_memVectorL2_zero_right_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (q : Vec d) : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system (0, q)).eval x)).2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_upperImage_memVectorL2_zero_right_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (q : Vec d) : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system (0, q)).eval x)).1

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredLowerImage_potential_zeroRight_of_elliptic_hodge {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system (0, q)).eval x)).2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredLowerImage_potential_zeroRight_of_elliptic_convex {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system (0, q)).eval x)).2

Convex-domain version of the zero-right lower-image potential recovery.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_mem_responseSpace_zero_right_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hU : IsSobolevRegularDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : BlockResponseSpace a U (R.recoveredField system (0, q))

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_mem_responseSpace_zero_right_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hU : IsSobolevRegularDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) [HasHodgeConverse U] (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : BlockResponseSpace a U (R.recoveredField system (0, q))

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_mem_responseSpace_zero_right_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : BlockResponseSpace a U (R.recoveredField system (0, q))

Convex-domain recovery wrapper for the zero-right response-space witness. This is the preferred Chapter-2-facing surface when the domain is known to be bounded open convex: no abstract HasHodgeConverse package is required.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_upperImage_isSolenoidalOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : IsSolenoidalOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system P).eval x)).1

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_lowerImage_memVectorL2_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (P : BlockVec d) : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system P).eval x)).2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_upperImage_memVectorL2_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (P : BlockVec d) : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system P).eval x)).1

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_lowerImage_isPotential_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system P).eval x)).2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_lowerImage_isPotential_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((R.recoveredField system P).eval x)).2

Convex-domain version of the lower-image potential recovery.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_mem_responseSpace_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hU : IsSobolevRegularDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : BlockResponseSpace a U (R.recoveredField system P)

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_mem_responseSpace_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hU : IsSobolevRegularDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) [HasHodgeConverse U] (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : BlockResponseSpace a U (R.recoveredField system P)

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_mem_blockResponseSpace {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : BlockResponseSpace a U (R.recoveredField system P)

Convex-domain recovery wrapper for the full block response-space witness. This keeps the concrete bounded-open-convex Hodge theorem visible at the public recovery surface.