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

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

Mu correction-space recovery -- definitions and pairing identities

Basic defs: correctionPart, recoveredCorrectionField, recoveredField; the linearity (add, smul) and memBlockL2 / admissible witnesses; pairing integrability / averages on openCubeSet and cubeSet; the minimizer_eq identity, and the blockPairingAverage / integral_blockPairing = 0 lemmas for repr_recoveredField and correction.

noncomputable def HCPolySupport.MuCorrectionSpaceRecoveryData.correctionPart {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : ↥↑R.correctionSpace

The correction part of the Hilbert minimizer, viewed inside the recovered correction subspace.

Equations

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

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.correctionPart_add {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P Q : BlockVec d) : R.correctionPart system (P + Q) = R.correctionPart system P + R.correctionPart system Q

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.correctionPart_smul {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (c : ℝ) (P : BlockVec d) : R.correctionPart system (c • P) = c • R.correctionPart system P

noncomputable def HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredCorrectionField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : CorrectionFieldData U

The recovered correction field realizing the correction part of the Hilbert minimizer.

Equations

• R.recoveredCorrectionField system P = R.repr (R.correctionPart system P)

noncomputable def HCPolySupport.MuCorrectionSpaceRecoveryData.affineField {d : ℕ} {U : Set (Vec d)} (R : MuCorrectionSpaceRecoveryData U) (P : BlockVec d) (Y : ↥↑R.correctionSpace) : BlockState d

The affine block state built from a fixed datum P and an arbitrary recovered correction-space element.

Equations

• R.affineField P Y = { potential := (fun (x : HCPolySupport.Vec d) => P.1) + (R.repr Y).potential, flux := (fun (x : HCPolySupport.Vec d) => P.2) + (R.repr Y).flux }

noncomputable def HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : BlockState d

The recovered pointwise minimizer field obtained from the recovered correction part and the constant datum P.

Equations

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

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.affineField_correctionPart {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : R.affineField P (R.correctionPart system P) = R.recoveredField system P

The generic affine field specializes to the minimizer-built recovered field when the correction is chosen to be correctionPart.

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.affineField_memBlockL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (P : BlockVec d) (Y : ↥↑R.correctionSpace) : MemBlockL2 U (R.affineField P Y).eval

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.affineField_admissible {d : ℕ} {U : Set (Vec d)} (R : MuCorrectionSpaceRecoveryData U) (P : BlockVec d) (Y : ↥↑R.correctionSpace) : IsBlockMuAdmissible U P (R.affineField P Y)

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.affineField_hilbert_eq_const_add {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (P : BlockVec d) (Y : ↥↑R.correctionSpace) : toHilbertBlockL2OfBlockField ⋯ = blockVecToHilbertBlockL2Const P + ↑Y

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_add {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P Q : BlockVec d) : R.recoveredField system (P + Q) = R.recoveredField system P + R.recoveredField system Q

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_smul {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (c : ℝ) (P : BlockVec d) : R.recoveredField system (c • P) = c • R.recoveredField system P

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_memBlockL2 {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : MemBlockL2 U (R.recoveredField system P).eval

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_admissible {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : IsBlockMuAdmissible U P (R.recoveredField system P)

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_integral_pairing_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n))) (system : MuOperatorSystemData (openCubeSet (originCube d n)) a) (P : BlockVec d) : ∫ (x : Vec d) in openCubeSet (originCube d n), vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x) = (MeasureTheory.volume (openCubeSet (originCube d n))).toReal * vecDot P.1 P.2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_integral_pairing_cubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n))) (system : MuOperatorSystemData (cubeSet (originCube d n)) a) (P : BlockVec d) : ∫ (x : Vec d) in cubeSet (originCube d n), vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x) = (MeasureTheory.volume (cubeSet (originCube d n))).toReal * vecDot P.1 P.2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_integrableOn_pairing_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n))) (system : MuOperatorSystemData (openCubeSet (originCube d n)) a) (P : BlockVec d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x)) (openCubeSet (originCube d n)) MeasureTheory.volume

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_integrableOn_pairing_cubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n))) (system : MuOperatorSystemData (cubeSet (originCube d n)) a) (P : BlockVec d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x)) (cubeSet (originCube d n)) MeasureTheory.volume

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_average_pairing_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n))) (system : MuOperatorSystemData (openCubeSet (originCube d n)) a) (P : BlockVec d) : (volumeAverage (openCubeSet (originCube d n)) fun (x : Vec d) => vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x)) = vecDot P.1 P.2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_average_pairing_cubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n))) (system : MuOperatorSystemData (cubeSet (originCube d n)) a) (P : BlockVec d) : (volumeAverage (cubeSet (originCube d n)) fun (x : Vec d) => vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x)) = vecDot P.1 P.2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_average_state_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n))) (system : MuOperatorSystemData (openCubeSet (originCube d n)) a) (P : BlockVec d) : (fun (i : Fin d) => volumeAverage (openCubeSet (originCube d n)) fun (x : Vec d) => (R.recoveredField system P).potential x i, fun (i : Fin d) => volumeAverage (openCubeSet (originCube d n)) fun (x : Vec d) => (R.recoveredField system P).flux x i) = P

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_average_state_cubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} (R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n))) (system : MuOperatorSystemData (cubeSet (originCube d n)) a) (P : BlockVec d) : (fun (i : Fin d) => volumeAverage (cubeSet (originCube d n)) fun (x : Vec d) => (R.recoveredField system P).potential x i, fun (i : Fin d) => volumeAverage (cubeSet (originCube d n)) fun (x : Vec d) => (R.recoveredField system P).flux x i) = P

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_average_state_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hU : IsSobolevRegularDomain U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => (R.recoveredField system P).potential x i, fun (i : Fin d) => volumeAverage U fun (x : Vec d) => (R.recoveredField system P).flux x i) = P

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_integrableOn_pairing_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x)) U MeasureTheory.volume

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_average_pairing_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (hpotZero : ∀ (P : BlockVec d), (fun (i : Fin d) => ∫ (x : Vec d) in U, (R.recoveredCorrectionField system P).potential x i) = 0) (hfluxZero : ∀ (P : BlockVec d), (fun (i : Fin d) => ∫ (x : Vec d) in U, (R.recoveredCorrectionField system P).flux x i) = 0) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (P : BlockVec d) : (volumeAverage U fun (x : Vec d) => vecDot ((R.recoveredField system P).potential x) ((R.recoveredField system P).flux x)) = vecDot P.1 P.2

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_minimizer_eq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) : toHilbertBlockL2OfBlockField ⋯ = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).minimizerMap P

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.blockPairingAverage_repr_recoveredField_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) (Y : ↥↑R.correctionSpace) : blockPairingAverage U a { potential := (R.repr Y).potential, flux := (R.repr Y).flux } (R.recoveredField system P) = 0

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.integral_blockPairingIntegrand_repr_recoveredField_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) (Y : ↥↑R.correctionSpace) (hvol : (MeasureTheory.volume U).toReal ≠ 0) : ∫ (x : Vec d) in U, blockPairingIntegrand a { potential := (R.repr Y).potential, flux := (R.repr Y).flux } (R.recoveredField system P) x = 0

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.blockPairingAverage_correction_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) (hpot : IsPotentialZeroTraceOn U f) (hsol : IsSolenoidalZeroNormalTraceOn U g) : blockPairingAverage U a { potential := f, flux := g } (R.recoveredField system P) = 0

theorem HCPolySupport.MuCorrectionSpaceRecoveryData.integral_blockPairingIntegrand_correction_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) (hpot : IsPotentialZeroTraceOn U f) (hsol : IsSolenoidalZeroNormalTraceOn U g) (hvol : (MeasureTheory.volume U).toReal ≠ 0) : ∫ (x : Vec d) in U, blockPairingIntegrand a { potential := f, flux := g } (R.recoveredField system P) x = 0