High-contrast homogenization: Provider.Entry.AdapterForward

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

The forward half of the adapted-to-Euclidean comparison

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

E_n^q - F_k ≤ C_AE(d)𝔢_qΓ_{g,S}(k)3^{-(n-k)}𝐄 for 0 ≤ k < n.

The adapted cell ⋄_n^q is filled by the Euclidean cells and the rows split at the comparison generation. A row at or above it is paid by the annealed mean order on the Euclidean cubes — every cube of a generation r ≥ k has annealed block below F_k, and the rows together carry relative volume at most one. A row below it is paid by the Euclidean cell bound E[𝐀(z+□_r)] ≤ (1+9K_{Ψ_S}^23^{-r})^g𝐄 against the cross-grid row weight C_d|q^{-1}|3^{r-n}, and the geometric series Entry.sum_belowSplit_le totals them at the printed 20Γ_{g,S}(k)3^{-(n-k)}.

Only finitely many rows can be averaged at once, so the rows below an explicitly chosen cutoff are kept pathwise, in the crude majorant of AdapterMajorant; the cutoff is chosen so that the mean of that tail is under one fifth of a unit of the printed error. No limit is taken: the exhaustion of e.two.grid.whitney.average already contains the passage to the limit, and what is fed to it is a majorant of every finite partial sum.

The exhibited constant of this half is the printed one, 122d^{3/2}; the cross-grid factor |q^{-1}| ≤ 101/100 carries no eccentricity.

There are no definitions in this file.

theorem HCPolySupport.HighContrast.Entry.adaptedMean_sub_centeredCube_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) {q : Mat d} (hq : Matrix.PosDef q) (hqinv : ‖q⁻¹‖ ≤ 101 / 100) {k n : ℤ} (hk : 0 ≤ k) (hkn : k < n) : BlockMatLoewnerLE (blockSub (annealedBlock P (adaptedCell q n)) (annealedBlock P (centeredCube d k))) (blockScale (122 * ↑d * √↑d * transferGauge g K k * 3 ^ (k - n)) E)

The forward half of the adapted-to-Euclidean comparison. For 0 ≤ k < n the adapted mean at generation n exceeds the Euclidean mean at generation k by at most C_AE(d)Γ_{g,S}(k)3^{-(n-k)}𝐄, with the exhibited constant C_AE(d) = 122d^{3/2}; the cross-grid factor is |q^{-1}| ≤ 101/100 and carries no eccentricity.