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

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

Mu recovery -- Minimizer and PotentialSolenoidalL2 package APIs

MuMinimizerRecoveryData namespace (ofCorrectionSpaceRecovery and the hasQuadraticMu / exists_coarseBlockMatrix / mu_eq_half_blockVecDot bridges) plus the PotentialSolenoidalL2RecoveryData API used by the origin-cube recovery layer.

noncomputable def HCPolySupport.MuMinimizerRecoveryData.toLinearMuMinimizerFamily {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuMinimizerRecoveryData U a) : LinearMuMinimizerFamily U a

Convert recovery data for Hilbert minimizers into the note-faithful linear family of pointwise doubled minimizers.

Equations

• M.toLinearMuMinimizerFamily = { field := M.field, map_add := ⋯, map_smul := ⋯, admissible := ⋯, pairingIntegrable := ⋯, realizes := ⋯ }

theorem HCPolySupport.MuMinimizerRecoveryData.hasQuadraticMu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuMinimizerRecoveryData U a) : HasQuadraticMu U a

theorem HCPolySupport.MuMinimizerRecoveryData.exists_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuMinimizerRecoveryData U a) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.MuMinimizerRecoveryData.existsUnique_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuMinimizerRecoveryData U a) : ∃! Abar : BlockMat d, IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.MuMinimizerRecoveryData.mu_eq_half_blockVecDot_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuMinimizerRecoveryData U a) (P : BlockVec d) : Mu U P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)

noncomputable def HCPolySupport.MuMinimizerRecoveryData.ofCorrectionSpaceRecovery {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (system : MuOperatorSystemData U a) (R : MuCorrectionSpaceRecoveryData U) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) U MeasureTheory.volume) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) : MuMinimizerRecoveryData U a

Build minimizer recovery data from a recovered correction space, leaving pairing integrability as the only remaining auxiliary input.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toMuHilbertRealization {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) : MuHilbertRealization U a

The Hilbert-space realization associated with the block-side recovery data and a concrete doubled operator system.

Equations

• R.toMuHilbertRealization system = system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData

structure HCPolySupport.PotentialSolenoidalL2RecoveryData.MuRecoveryCompatibilityData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) : Prop

The remaining recovery-side hypotheses needed to convert the Hilbert minimization package into the note-faithful pointwise minimizer family.

• pairingIntegrable (P Q : BlockVec d) : MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.toMuCorrectionSpaceRecoveryData.recoveredField system P) (R.toMuCorrectionSpaceRecoveryData.recoveredField system Q)) U MeasureTheory.volume
• mu_eq_muCandidate (P : BlockVec d) : Mu U P a = (R.toMuHilbertRealization system).muCandidate P

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.muRecoveryData_of_ellipticity_candidateEquality {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (R.toMuHilbertRealization (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)).muCandidate P) : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)

Under ellipticity, the only non-formal field of MuRecoveryCompatibilityData is the identification of Mu with the Hilbert minimizer value. Pairing integrability follows automatically from the L² control of recovered fields.

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toLinearMuMinimizerFamily {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) (compat : R.MuRecoveryCompatibilityData system) : LinearMuMinimizerFamily U a

The linear minimizer family produced directly from block-side recovery data and a concrete doubled operator system.

Equations

• R.toLinearMuMinimizerFamily system compat = (HCPolySupport.MuMinimizerRecoveryData.ofCorrectionSpaceRecovery system R.toMuCorrectionSpaceRecoveryData ⋯ ⋯).toLinearMuMinimizerFamily

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toMuMinimizerRecoveryData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) (compat : R.MuRecoveryCompatibilityData system) : MuMinimizerRecoveryData U a

Build minimizer recovery data directly from block-side recovery data \Lpoto(U) × \Lsolo(U) and a concrete doubled operator system.

Equations

• R.toMuMinimizerRecoveryData system compat = HCPolySupport.MuMinimizerRecoveryData.ofCorrectionSpaceRecovery system R.toMuCorrectionSpaceRecoveryData ⋯ ⋯

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.hasQuadraticMu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) (compat : R.MuRecoveryCompatibilityData system) : HasQuadraticMu U a

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.exists_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) (compat : R.MuRecoveryCompatibilityData system) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.existsUnique_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) (compat : R.MuRecoveryCompatibilityData system) : ∃! Abar : BlockMat d, IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_eq_half_blockVecDot_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (system : MuOperatorSystemData U a) (compat : R.MuRecoveryCompatibilityData system) (P : BlockVec d) : Mu U P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toMuOperatorSystemDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : MuOperatorSystemData U a

The deterministic doubled operator system built from raw ellipticity and the packaged block-side correction space.

Equations

• R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol = R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toMuMinimizerRecoveryDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : MuMinimizerRecoveryData U a

Build minimizer recovery data directly from block-side recovery data and raw ellipticity assumptions.

Equations

• R.toMuMinimizerRecoveryDataOfIsEllipticFieldOn hEll hvol compat = R.toMuMinimizerRecoveryData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol) compat

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.hasQuadraticMuOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : HasQuadraticMu U a

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.exists_coarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.existsUnique_coarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : ∃! Abar : BlockMat d, IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_eq_half_blockVecDot_coarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (P : BlockVec d) : Mu U P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_zero_right_eq_responseJ_zero_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {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) (hdet : IsUnit (Matrix.det sigmaStar)) (q : Vec d) : Mu U (0, q) a = ResponseJ U 0 q a

Under the deterministic coarse-data package, the recovery-side quadratic representation of \mu identifies its pure-flux slice with the scalar response slice \mathcal J(U; 0, q, a).

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_left_zero_eq_responseJ_zero_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {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) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : Mu U (p, 0) a = ResponseJ U p 0 a

Under the deterministic coarse-data package, the recovery-side quadratic representation of \mu identifies its pure-gradient slice with the scalar response slice \mathcal J(U; p, 0, a).

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.coarseMatrix_lowerRight_eq_sigmaStarInvCoarse_of_ellipticField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (hMuResp : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a) : (coarseBlockMatrix U a).lowerRight = sigmaStarInvCoarse U a

If the pure-flux slice of \mu matches the pure-flux slice of \mathcal J, then the lower-right block of \mathbf A(U; a) is the canonical \sigma_*^{-1}(U; a), packaged directly from recovery data and ellipticity.

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.coarseStarredBlockMatrixInv_upperLeft_eq_sigmaStarInvCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (hMuResp : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a) : (coarseStarredBlockMatrixInv U a).upperLeft = sigmaStarInvCoarse U a

If the pure-flux slice of \mu matches the pure-flux slice of \mathcal J, then the upper-left block of \mathbf A_*^{-1}(U; a) is the canonical \sigma_*^{-1}(U; a), packaged directly from recovery data and ellipticity.

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_ge_vecDot_of_isEllipticFieldOn {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) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (P : BlockVec d) : vecDot P.1 P.2 ≤ Mu U P a

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_ge_vecDot_openCubeSet_originCubeOfIsEllipticFieldOn {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) (P : BlockVec d) : vecDot P.1 P.2 ≤ Mu (openCubeSet (originCube d n)) P a

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.mu_ge_vecDot_cubeSet_originCubeOfIsEllipticFieldOn {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (cubeSet (originCube d n))) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) (P : BlockVec d) : vecDot P.1 P.2 ≤ Mu (cubeSet (originCube d n)) P a