Coarse-graining support: Support.CoarseGraining.MuRecoveryBlockResponse

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

Direct convex-domain bridges from recovered fields to block-response pair-half representations and scalar-response splitting identities.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.exists_blockResponseHalfState_ae_eq_recoveredField_zero_right {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) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (R.recoveredField system (0, q)).eval x

Hodge-packaged direct recovery-to-half-pair bridge for the pure-flux slice. This is the generic form of the convex-domain wrapper below.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.exists_blockResponseHalfState_ae_eq_recoveredField_of_ellipticField {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) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (R.recoveredField system P).eval x

Hodge-packaged direct recovery-to-half-pair bridge for a general block datum. This is the generic form of the convex-domain wrapper below.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.mu_zeroRight_eq_responseJ_zero_of_HodgeConverse {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) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (q0 : Vec d) : Mu U (0, q0) a = ResponseJ U 0 q0 a

Recovery-to-response bridge for the pure-flux slice, proved without any coarse-matrix package. This is the sigma-free theorem needed before the canonical sigma_*^{-1} positivity layer.

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_zeroRight_eq_responseJ_zero_of_HodgeConverse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hU : IsSobolevRegularDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (q0 : Vec d) : Mu U (0, q0) a = ResponseJ U 0 q0 a

Packaged pure-flux recovery/response bridge on a Hodge domain.

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_zeroRight_eq_responseJ_zero_of_ConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (q0 : Vec d) : Mu U (0, q0) a = ResponseJ U 0 q0 a

Preferred convex-domain wrapper for the packaged pure-flux recovery/response bridge.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.exists_responseHalfState_ae_eq_recoveredZeroRight {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) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (R.recoveredField system (0, q)).eval x

Convex-domain direct recovery-to-half-pair bridge for the pure-flux slice. This packages the response-space and lower-image-potential promotion into a single theorem, so downstream users can recover the scalar primal/adjoint pair without mentioning any Hodge or response-space intermediate hypotheses.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.exists_responseHalfState_ae_eq_recoveredField {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) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (R.recoveredField system P).eval x

Convex-domain direct recovery-to-half-pair bridge for a general block datum.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.mu_zeroLeft_eq_responseJ_zero_of_ConvexDomain {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) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (p0 : Vec d) : Mu U (p0, 0) a = ResponseJ U p0 0 a

Recovery-to-response bridge for the pure-gradient slice, proved without any coarse-matrix package.

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_zeroLeft_eq_responseJ_zero_of_ConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (p0 : Vec d) : Mu U (p0, 0) a = ResponseJ U p0 0 a

Packaged pure-gradient recovery/response bridge on a bounded open convex domain.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.responseJ_eq_mu_negLeft_sub_vecDot {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) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (p0 q0 : Vec d) : ResponseJ U p0 q0 a = Mu U (-p0, q0) a - vecDot p0 q0

Recovery-to-response bridge for the full mixed slice, proved without any coarse-matrix package.

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.responseJ_eq_mu_negLeft_sub_vecDot {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (p0 q0 : Vec d) : ResponseJ U p0 q0 a = Mu U (-p0, q0) a - vecDot p0 q0

Packaged full mixed recovery/response bridge on a bounded open convex domain.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.volumeAverage_blockResponse_eq_scalarSum_recoveredZeroRight {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) (q0 p pStar q qStar : Vec d) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), volumeAverage U (blockResponseIntegrand a (p, q) (qStar, pStar) (R.recoveredField system (0, q0))) = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a (p - pStar) (qStar - q) u) + 1 / 2 * volumeAverage U (scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v)

Convex-domain direct scalar-response splitting for the pure-flux recovered field. This is the note-facing form of the previous bridge.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.volumeAverage_blockResponse_eq_scalarSum_recovered {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) (p pStar q qStar : Vec d) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), volumeAverage U (blockResponseIntegrand a (p, q) (qStar, pStar) (R.recoveredField system P)) = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a (p - pStar) (qStar - q) u) + 1 / 2 * volumeAverage U (scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v)

Convex-domain direct scalar-response splitting for a general recovered block datum.