High-contrast homogenization: Provider.Response.PreYoungFixedGridNestedRows

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

Nested row pairings at every fine scale, fixed grid

The nested row pairings at every fine scale on a fixed rounded grid: the grid stays rounded at the fixed alignment l while the generation window {s, t} moves, the aligned-cell integrability coming from the AlignedCellsIntegrable carrier instead of the window multiplier's carrier equality. The proof is unchanged apart from the window bundle replaced by the carrier.

theorem HCPolySupport.HighContrast.Response.FixedGrid.nestedAnnealedCellPairings_primal_le_of_cells {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hcells : AlignedCellsIntegrable P q s t) (hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) {k : ℤ} (hks : k ≤ s) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k s) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) : (avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Qcen (blockCellAverage (adaptedCellAt q k (nestedLabel k s z w)) (diagonalWeakState ⋯ t (a.subSkew g hg) p r)).1| ∂P) ≤ profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => a.subSkew g hg) p r * profileSchurLoadFlux (profileHattedBlock g (annealedBlock P (adaptedCellAt q k w))) Qcen ∧ (avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Pcen (blockCellAverage (adaptedCellAt q k (nestedLabel k s z w)) (diagonalWeakState ⋯ t (a.subSkew g hg) p r)).2| ∂P) ≤ profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => a.subSkew g hg) p r * profileSchurLoadGradient (profileHattedBlock g (annealedBlock P (adaptedCellAt q k w))) Pcen

The primal nested row pairing remains valid at every fine scale. Above the starting scale it uses stationary finite means; below that scale it uses the source-window enclosure and the parent-aligned stationarity relation.

theorem HCPolySupport.HighContrast.Response.FixedGrid.nestedAnnealedCellPairings_adjoint_le_of_cells {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hcells : AlignedCellsIntegrable P q s t) (hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) {k : ℤ} (hks : k ≤ s) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k s) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) : (avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Qcen (blockCellAverage (adaptedCellAt q k (nestedLabel k s z w)) (diagonalWeakAdjointState ⋯ t (a.subSkew g hg) p r)).1| ∂P) ≤ profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => (a.subSkew g hg).transpose) p r * profileSchurLoadFlux (profileHattedAdjointBlock g (annealedBlock P (adaptedCellAt q k w))) Qcen ∧ (avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Pcen (blockCellAverage (adaptedCellAt q k (nestedLabel k s z w)) (diagonalWeakAdjointState ⋯ t (a.subSkew g hg) p r)).2| ∂P) ≤ profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => (a.subSkew g hg).transpose) p r * profileSchurLoadGradient (profileHattedAdjointBlock g (annealedBlock P (adaptedCellAt q k w))) Pcen

The adjoint nested row pairing remains valid at every fine scale allowed by the source-window telescope.