High-contrast homogenization: Provider.Response.PreYoungFixedGridCells

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

Aligned-cell integrability on a fixed rounded grid

The pre-Young chain obtains the integrable coarse blocks of the aligned source cells from the window multiplier, through the literal carrier equality q = roundedGrid jStar m0 tying the grid's rounding scale to the moving source alignment. The paper's fixed-grid recurrence (q = roundedGrid lAl m0 with lAl fixed and the generation window moving) cannot satisfy that equality, so the fixed-grid chain replaces the window multiplier by the exact integrability carrier below, constructed here directly from the coarse ellipticity e.coarse.ellipticity.

def HCPolySupport.HighContrast.Response.FixedGrid.AlignedCellsIntegrable {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (s t : ℤ) : Prop

The aligned-cell integrability carrier. Every aligned subcell of either source cell of the window {s, t} has an integrable coarse response. This is exactly the content that the moving-window chain draws from the window multiplier, isolated from the multiplier's carrier equality.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.FixedGrid.alignedCellsIntegrable_of_dagger {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) : AlignedCellsIntegrable P q s t

Under the coarse ellipticity e.coarse.ellipticity, every adapted cell of every positive-definite grid has an integrable coarse response; in particular the aligned-cell integrability carrier holds on every window.