High-contrast homogenization: Provider.Response.PreYoungAllScaleNestedStationarity

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Stationarity along nested cells below the alignment scale

Although a fine-scale cell need not itself have an integral center, moving between two copies of that cell inside aligned parent cells is an integer translation. This is the stationarity relation needed by finite projection arguments whose child depth tends to infinity.

theorem HCPolySupport.HighContrast.Response.exists_translateSet_adaptedCellAt_nestedLabel_of_parent_aligned {d : ℕ} {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k s : ℤ} (hks : k ≤ s) (hls : l ≤ s) (z w : Fin d → ℤ) : ∃ (v : Fin d → ℤ), adaptedCellAt q k (nestedLabel k s z w) = translateSet (Source.AKL.intTranslation v) (adaptedCellAt q k w)

A nested fine cell is an integer translate of the reference fine cell whenever the parent scale is aligned. No alignment assumption is needed at the fine scale.

theorem HCPolySupport.HighContrast.Response.annealedBlock_adaptedCellAt_nestedLabel_eq_of_parent_aligned {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k s : ℤ} (hks : k ≤ s) (hls : l ≤ s) (z w : Fin d → ℤ) (hmeas : HasMeasurableCoarseBlock P (adaptedCellAt q k w)) : annealedBlock P (adaptedCellAt q k (nestedLabel k s z w)) = annealedBlock P (adaptedCellAt q k w)

The annealed block is unchanged between nested copies of a fine cell when the displacement comes from an aligned parent scale.

theorem HCPolySupport.HighContrast.Response.profileSchurLoadFlux_nestedLabel_eq_of_parent_aligned {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k s : ℤ} (hks : k ≤ s) (hls : l ≤ s) (z w : Fin d → ℤ) (hmeas : HasMeasurableCoarseBlock P (adaptedCellAt q k w)) (h : Mat d) (Qcen : Vec d) : profileSchurLoadFlux (profileHattedBlock h (annealedBlock P (adaptedCellAt q k (nestedLabel k s z w)))) Qcen = profileSchurLoadFlux (profileHattedBlock h (annealedBlock P (adaptedCellAt q k w))) Qcen

Parent alignment preserves the primal flux load between nested copies of a fine cell.

theorem HCPolySupport.HighContrast.Response.profileSchurLoadGradient_nestedLabel_eq_of_parent_aligned {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k s : ℤ} (hks : k ≤ s) (hls : l ≤ s) (z w : Fin d → ℤ) (hmeas : HasMeasurableCoarseBlock P (adaptedCellAt q k w)) (h : Mat d) (Pcen : Vec d) : profileSchurLoadGradient (profileHattedBlock h (annealedBlock P (adaptedCellAt q k (nestedLabel k s z w)))) Pcen = profileSchurLoadGradient (profileHattedBlock h (annealedBlock P (adaptedCellAt q k w))) Pcen

Parent alignment preserves the primal gradient load between nested copies of a fine cell.

theorem HCPolySupport.HighContrast.Response.profileSchurLoadFlux_adjoint_nestedLabel_eq_of_parent_aligned {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k s : ℤ} (hks : k ≤ s) (hls : l ≤ s) (z w : Fin d → ℤ) (hmeas : HasMeasurableCoarseBlock P (adaptedCellAt q k w)) (h : Mat d) (Qcen : Vec d) : profileSchurLoadFlux (profileHattedAdjointBlock h (annealedBlock P (adaptedCellAt q k (nestedLabel k s z w)))) Qcen = profileSchurLoadFlux (profileHattedAdjointBlock h (annealedBlock P (adaptedCellAt q k w))) Qcen

Parent alignment preserves the adjoint flux load between nested copies of a fine cell.

theorem HCPolySupport.HighContrast.Response.profileSchurLoadGradient_adjoint_nestedLabel_eq_of_parent_aligned {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k s : ℤ} (hks : k ≤ s) (hls : l ≤ s) (z w : Fin d → ℤ) (hmeas : HasMeasurableCoarseBlock P (adaptedCellAt q k w)) (h : Mat d) (Pcen : Vec d) : profileSchurLoadGradient (profileHattedAdjointBlock h (annealedBlock P (adaptedCellAt q k (nestedLabel k s z w)))) Pcen = profileSchurLoadGradient (profileHattedAdjointBlock h (annealedBlock P (adaptedCellAt q k w))) Pcen

Parent alignment preserves the adjoint gradient load between nested copies of a fine cell.