Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.OneStepContraction.CenteredResponses

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

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

Centered-response identities for the one-step contraction #

This file proves the Section 5.4 special-vector bridge from the Section 5.2 centered-response identities to the scalar contrast Theta_m - 1.

source
theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.thetaAtScale_sub_one_eq_centeredResponses_special_of_vecNormSq_eq_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : vecNormSq e = 1) :
thetaAtScale hP hStruct ↑m - 1 = expectedCenteredResponseJAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e) + expectedCenteredResponseJStarAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e)

Special-vector centered responses sum to Theta_m - 1 for vectors with unit squared norm.

source
theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.thetaAtScale_sub_one_eq_centeredResponses_special {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : Ch02.vecNorm e = 1) :
thetaAtScale hP hStruct ↑m - 1 = expectedCenteredResponseJAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e) + expectedCenteredResponseJStarAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e)

Special-vector centered responses sum to Theta_m - 1 for unit vectors, in the same norm convention used by the good-scale theorem.

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

The centered adjoint response has the same expectation as the centered primal response. This is the Section 5.2 identity in a rewrite-friendly form for the one-step proof.

source
theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.thetaAtScale_sub_one_eq_two_centeredResponse_special {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : Ch02.vecNorm e = 1) :
thetaAtScale hP hStruct ↑m - 1 = 2 * expectedCenteredResponseJAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e)

Special-vector form of the one-step centered-response identity using only the primal centered response.