High-contrast homogenization: Provider.Entry.AdapterReverseRows

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

The adapted filling of a Euclidean cube

The second estimate of the comparison between adapted and Euclidean cubes:

F_m - E_n^q ≤ C_AE𝔢_qΓ_{g,S}(n)3^{-(m-n)}𝐄 for ℓ_al ≤ n < m.

Here the Euclidean cube □_m is the target and the adapted cells fill it, so the printed cross-grid factor is |q|, at most (100/99)𝔢_q by e.rounded.grid.bounds. The rows read as follows.

The starting row. The scale-n cells of the filling are integer translates of ⋄_n^q — this is the aligned-subdivision property of the coarse block taken from HC — so each has annealed block exactly E_n^q, and the rows together carry relative volume at most one.

The rows below the starting scale. A cell there is an adapted cell of a lower generation, which e.coarse.ellipticity does not bound directly: the coarse ellipticity condition speaks of standard cubes. What bounds it is its own Euclidean filling, and Entry.annealedBlock_adaptedCellAt_le performs that reading once and for all, at the cost of the one geometric series (1-g)^{-1} the filling carries. The cross-grid row weight C_d|q|3^{r-m} against that bound is then summed by Entry.sum_belowSplit_le at the printed rate 20Γ_{g,S}(n)3^{-(m-n)}.

The consequence for the constant is recorded where it is exhibited: this half's constant carries the extra (1-g)^{-1} of the composed reading, so the constant of the comparison is C_AE(d,g) rather than the printed C_AE(d). The frozen consumer obligation of p.response.transfer binds the constant after the burn exponent, so the dependence is admissible there.

There are no definitions in this file.

The pathwise rows majorant of a Euclidean cube

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_centeredCube_le_rows {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {q : Mat d} (hq : Matrix.PosDef q) {n m J : ℤ} (hm : 0 ≤ m) (hJn : J ≤ n) {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (s : ℤ), ↑(Z s) = Transport.fillingIndex q n (adaptedCellTranslate 1 m 0) s) : ∀ᵐ (a : CoeffSpace d) ∂P, toFullBlockMat (coarseBlock (adaptedCellTranslate 1 m 0) a) ≤ ∑ r ∈ Finset.Icc J n, ∑ w ∈ Z r, ((MeasureTheory.volume (adaptedCellAt q r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate 1 m 0)).toReal) • toFullBlockMat (coarseBlock (adaptedCellAt q r w) a) + (6 * ↑d * √↑d * ‖q‖ * ((2 * (6 * ↑d * √↑d * ‖q⁻¹‖) * (1 - g)⁻¹ + 1) * (3 ^ J + 3 ^ m + 3 * S a) * (2 * (1 - g)⁻¹ * (3 ^ (-m) * 3 ^ (↑J * (1 - g)))))) • toFullBlockMat E

The pathwise majorant of the adapted filling of a Euclidean cube. The coarse response of □_m lies below the weighted rows of the adapted filling from an arbitrary cutoff up to the starting generation, plus a tail whose coefficient is affine in the source scale. Each cell below the cutoff is paid by its own Euclidean filling, through the pathwise elliptic bound of AdapterCellBounds.