Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.MuRecovery.CorrectionSpaceEnergy

Coarse-graining support: Support.CoarseGraining.MuRecovery.CorrectionSpaceEnergy #

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

Mu correction-space recovery -- block-energy and mu lower bound #

recoveredField_blockEnergyAverage_eq_mu plus its >= vecDot variants (general, openCubeSet, cubeSet) and the mu_ge_vecDot theorems on origin cubes.

source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.quadraticEnergy_const_add_eq_blockEnergyAverage_affineField {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) :
quadraticEnergy (energyBilinOfOperator system.toMuOperatorRealization.operator) (blockVecToHilbertBlockL2Const P + ↑Y) = blockEnergyAverage U a (R.affineField P Y)
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.muCandidate_le_blockEnergyAverage_affineField {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) :
(system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P ≤ blockEnergyAverage U a (R.affineField P Y)
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.blockEnergyAverage_affineField_correctionPart_eq_muCandidate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) :
blockEnergyAverage U a (R.affineField P (R.correctionPart system P)) = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.muCandidate_eq_sInf_blockEnergyAverage_affineField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) :
(system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P = sInf (Set.range fun (Y : ↥↑R.correctionSpace) => blockEnergyAverage U a (R.affineField P Y))
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.continuous_blockEnergyAverage_affineField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (P : BlockVec d) :
Continuous fun (Y : ↥↑R.correctionSpace) => blockEnergyAverage U a (R.affineField P Y)
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.muCandidate_eq_sInf_blockEnergyAverage_affineField_denseSeq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : MuOperatorSystemData U a) (P : BlockVec d) :
(system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P = sInf (Set.range fun (n : ℕ) => blockEnergyAverage U a (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)))
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.muCandidate_eq_iInf_blockEnergyAverage_affineField_denseSeq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : MuOperatorSystemData U a) (P : BlockVec d) :
(system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P = ⨅ (n : ℕ), blockEnergyAverage U a (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n))
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.Mu_eq_sInf_blockEnergyAverage_affineField_denseSeq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : MuOperatorSystemData U a) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
Mu U P a = sInf (Set.range fun (n : ℕ) => blockEnergyAverage U a (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)))
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.Mu_eq_iInf_blockEnergyAverage_affineField_denseSeq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : MuOperatorSystemData U a) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
Mu U P a = ⨅ (n : ℕ), blockEnergyAverage U a (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n))
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.Mu_eq_sInf_blockEnergyAverage_affineField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
Mu U P a = sInf (Set.range fun (Y : ↥↑R.correctionSpace) => blockEnergyAverage U a (R.affineField P Y))
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_blockEnergyAverage_eq_mu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : MuCorrectionSpaceRecoveryData U) (system : MuOperatorSystemData U a) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
blockEnergyAverage U a (R.recoveredField system P) = Mu U P a
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_blockEnergyAverage_ge_vecDot_of_isEllipticFieldOn_of_pairingAverage {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) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) U MeasureTheory.volume) (pairingDiagIntegrable : ∀ (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) (pairingAverage : ∀ (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) (P : BlockVec d) :
vecDot P.1 P.2 ≤ blockEnergyAverage U a (R.recoveredField system P)
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.mu_ge_vecDot_of_isEllipticFieldOn_of_pairingAverage {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) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) U MeasureTheory.volume) (pairingDiagIntegrable : ∀ (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) (pairingAverage : ∀ (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) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
vecDot P.1 P.2 ≤ Mu U P a
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.mu_ge_vecDot_of_isEllipticFieldOn_of_integral_eq_zero {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) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) U MeasureTheory.volume) (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) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu U P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
vecDot P.1 P.2 ≤ Mu U P a
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_blockEnergyAverage_ge_vecDot_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} {lam Lam : ℝ} (R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n))) (system : MuOperatorSystemData (openCubeSet (originCube d n)) a) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) (openCubeSet (originCube d n)) MeasureTheory.volume) (P : BlockVec d) :
vecDot P.1 P.2 ≤ blockEnergyAverage (openCubeSet (originCube d n)) a (R.recoveredField system P)
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.recoveredField_blockEnergyAverage_ge_vecDot_cubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} {lam Lam : ℝ} (R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n))) (system : MuOperatorSystemData (cubeSet (originCube d n)) a) (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) (cubeSet (originCube d n)) MeasureTheory.volume) (P : BlockVec d) :
vecDot P.1 P.2 ≤ blockEnergyAverage (cubeSet (originCube d n)) a (R.recoveredField system P)
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.mu_ge_vecDot_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} {lam Lam : ℝ} (R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n))) (system : MuOperatorSystemData (openCubeSet (originCube d n)) a) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) (openCubeSet (originCube d n)) MeasureTheory.volume) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu (openCubeSet (originCube d n)) P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
vecDot P.1 P.2 ≤ Mu (openCubeSet (originCube d n)) P a
source
theorem HCPolySupport.MuCorrectionSpaceRecoveryData.mu_ge_vecDot_cubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} {lam Lam : ℝ} (R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n))) (system : MuOperatorSystemData (cubeSet (originCube d n)) a) (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (pairingIntegrable : ∀ (P Q : BlockVec d), MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q)) (cubeSet (originCube d n)) MeasureTheory.volume) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu (cubeSet (originCube d n)) P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) :
vecDot P.1 P.2 ≤ Mu (cubeSet (originCube d n)) P a