High-contrast homogenization: Provider.Entry.AdapterCellMean

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

The annealed bound on an aligned adapted cell

Averaging the Euclidean filling of z + ⋄_r^q against the Euclidean cell bound E[𝐀(z+□_i)] ≤ (1+9K_{Ψ_S}^23^{-i})^g𝐄 and summing the geometric series gives E[𝐀(z+⋄_r^q)] ≤ C_d(1-g)^{-1}(1+9K_{Ψ_S}^23^{-r})^g𝐄 at every generation and every aligned centre, with C_d = 126d^{3/2}.

This is the bound e.coarse.ellipticity does not give directly: the dagger speaks of standard cubes, and an adapted cell is only reached through its own Euclidean filling. The single factor (1-g)^{-1} is the geometric series of that filling; it is what the composed reading of the reverse comparison spends over the printed boundary decomposition.

There are no definitions in this file.

theorem HCPolySupport.HighContrast.Entry.annealedBlock_adaptedCellAt_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) (r : ℤ) (w : Fin d → ℤ) : BlockMatLoewnerLE (annealedBlock P (adaptedCellAt q r w)) (blockScale (126 * ↑d * √↑d * (1 - g)⁻¹ * (1 + 9 * K ^ 2 * 3 ^ (-r)) ^ g) E)

The annealed bound on an aligned adapted cell. Averaging the Euclidean filling of z + ⋄_r^q against the Euclidean cell bound and summing the geometric series gives E[𝐀(z+⋄_r^q)] ≤ C_d(1-g)^{-1}(1+9K_{Ψ_S}^23^{-r})^g𝐄, at every generation and every aligned centre, with C_d = 126d^{3/2}. The one factor (1-g)^{-1} is the geometric series of the filling.