Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section52.CenteredResponses

Coarse-graining support: Support.Book.Ch05.Theorems.Section52.CenteredResponses #

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

Section 5.2 internals: CenteredResponses #

Centered primal and adjoint response identities.

source
theorem HCPolySupport.Book.Ch05.Section52.expectedJFormula_sub_centering_eq_centeredResponseExpectation {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) :
expectedJScalarFormula hP hStruct m p q - scalarizedResponseCenteringTerm hP hStruct m p q = centeredResponseExpectationFormula hP hStruct m p q
source
theorem HCPolySupport.Book.Ch05.Section52.integrable_restrictionCenteredResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsFiniteMeasure P] (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) (hJ : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet Q p q) P) :
MeasureTheory.Integrable (restrictionCenteredResponseJObservableCubeSet hP hStruct m Q p q) P
source
theorem HCPolySupport.Book.Ch05.Section52.integrable_restrictionCenteredResponseJStarObservableCubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsFiniteMeasure P] (hAdj : Ch04.RestrictionAdjointInvariantLaw P) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) (hJ : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet Q p q) P) :
MeasureTheory.Integrable (restrictionCenteredResponseJStarObservableCubeSet hP hStruct m Q p q) P
source
theorem HCPolySupport.Book.Ch05.Section52.integral_restrictionCenteredResponseJObservableCubeSet_eq_expectedResponseJCubeSet_sub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) (hJ : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet Q p q) P) :
∫ (a : RegCoeffField d), restrictionCenteredResponseJObservableCubeSet hP hStruct m Q p q a ∂P = Ch04.expectedResponseJCubeSet P Q p q - scalarizedResponseCenteringTerm hP hStruct m p q
source
theorem HCPolySupport.Book.Ch05.Section52.integral_restrictionCenteredResponseJStarObservableCubeSet_eq_expectedResponseJCubeSet_sub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hAdj : Ch04.RestrictionAdjointInvariantLaw P) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) (hJ : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet Q p q) P) :
∫ (a : RegCoeffField d), restrictionCenteredResponseJStarObservableCubeSet hP hStruct m Q p q a ∂P = Ch04.expectedResponseJCubeSet P Q p q - scalarizedResponseCenteringTerm hP hStruct m p q
source
theorem HCPolySupport.Book.Ch05.Section52.expectedCenteredResponseJAtScale_eq_annealedResponseJAtScale_sub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) (hJ : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) :
expectedCenteredResponseJAtScale hP hStruct m p q = Ch04.annealedResponseJAtScale P m p q - scalarizedResponseCenteringTerm hP hStruct m p q
source
theorem HCPolySupport.Book.Ch05.Section52.expectedCenteredResponseJStarAtScale_eq_annealedResponseJAtScale_sub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hAdj : Ch04.RestrictionAdjointInvariantLaw P) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) (hJ : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) :
expectedCenteredResponseJStarAtScale hP hStruct m p q = Ch04.annealedResponseJAtScale P m p q - scalarizedResponseCenteringTerm hP hStruct m p q
source
theorem HCPolySupport.Book.Ch05.Section52.expectedCenteredResponseJAtScale_eq_centeredResponseExpectationFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) (hBlock : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d m)) P) :
expectedCenteredResponseJAtScale hP hStruct m p q = centeredResponseExpectationFormula hP hStruct m p q

Note-facing primal centered-response expectation formula.

source
theorem HCPolySupport.Book.Ch05.Section52.expectedCenteredResponseJStarAtScale_eq_centeredResponseExpectationFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) (hBlock : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d m)) P) :
expectedCenteredResponseJStarAtScale hP hStruct m p q = centeredResponseExpectationFormula hP hStruct m p q

Note-facing adjoint centered-response expectation formula.

source
theorem HCPolySupport.Book.Ch05.Section52.centeredResponses_homogenizationScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (p q : Vec d) :
expectedCenteredResponseJAtScale hP hStruct (↑m) p q = centeredResponseExpectationFormula hP hStruct (↑m) p q ∧ expectedCenteredResponseJStarAtScale hP hStruct (↑m) p q = centeredResponseExpectationFormula hP hStruct (↑m) p q

Manuscript Lemma l.centered.responses.homogenization.scale, expectation identity part: the centered primal and adjoint responses have the same scalarized expectation.