High-contrast homogenization: Provider.Entry.AdapterReverse

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

The reverse half of the adapted-to-Euclidean comparison

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

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

The starting row of the adapted filling of □_m consists of integer translates of ⋄_n^q, so each of its cells has annealed block exactly E_n^q and the rows together carry relative volume at most one. Below the starting scale a cell is an adapted cell of a lower generation, which e.coarse.ellipticity does not bound directly; Entry.annealedBlock_adaptedCellAt_le bounds it through its own Euclidean filling, and the cross-grid row weight C_d|q|3^{r-m} against that bound is summed by Entry.sum_belowSplit_le at the printed rate 20Γ_{g,S}(n)3^{-(m-n)}.

The constant exhibited carries the extra (1-g)^{-1} of that composed reading.

There are no definitions in this file.

theorem HCPolySupport.HighContrast.Entry.centeredCube_sub_adaptedMean_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hd : 1 ≤ d) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {lAl : ℤ} {q : Mat d} (hgrid : IsRoundedGrid lAl q) (hqinv : ‖q⁻¹‖ ≤ 101 / 100) {n m : ℤ} (hlAl : lAl ≤ n) (hn : 0 ≤ n) (hnm : n < m) : BlockMatLoewnerLE (blockSub (annealedBlock P (centeredCube d m)) (adaptedMean P q n)) (blockScale ((15120 * ↑d ^ 3 * (1 - g)⁻¹ * ‖q‖ + 1) * transferGauge g K n * 3 ^ (n - m)) E)

The reverse half of the adapted-to-Euclidean comparison. For ℓ_al ≤ n < m the Euclidean mean at generation m exceeds the adapted mean at generation n by at most C𝔢_qΓ_{g,S}(n)3^{-(m-n)}𝐄. The constant exhibited here carries the extra (1-g)^{-1} of the composed reading of the boundary cells; the printed constant is dimension-only, and reaching it would need the boundary shell of the printed decomposition rather than the composed filling.