High-contrast homogenization: Provider.Entry.StandardCellMean

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

The Euclidean cell bound at every generation and every center

The boundary layers of the comparison between adapted and Euclidean cubes are unions of standard aligned cubes at generations running down to -∞, and they sit wherever the target cell sits, not at the origin. The printed proof handles them with the ellipticity of e.coarse.ellipticity and integer stationarity. Both are needed together, in the following form.

e.coarse.ellipticity discounts a cube by 3^{g(m-k)} only when the cube's center lies in the macroscopic cube □_m that the source has burned, so read literally on a cube deep inside a large target it costs a factor of the target's own generation. Integer stationarity removes that cost: a standard aligned cube of any generation is the integer translate of one whose center lies in the unit cube — at a nonnegative generation the center is integral, at a negative one the index reduces modulo 3^{-k} — and a cube centered in the unit cube burns at the macroscopic generation max{1, k+l}, where 3^l brackets 3^{-k}S.

The resulting mean bound E[𝐀(z+□_k)] ≤ (1 + 9K_{Ψ_S}^23^{-k})^g𝐄 holds at every generation k ∈ ℤ and every aligned center, which is exactly what the geometric-series calculation of the comparison consumes. Its only stochastic input is the source mean E[S] ≤ 2K_{Ψ_S}^2, moved inside the concave power by Jensen's inequality — the step the printed proof performs with Hölder.

There are no definitions in this file.

Jensen's inequality at an affine argument

theorem HCPolySupport.HighContrast.Entry.integral_rpow_affine_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {A B : ℝ} (hA : 1 ≤ A) (hB : 0 ≤ B) : ∫ (a : CoeffSpace d), (A + B * S a) ^ g ∂P ≤ (A + B * ∫ (a : CoeffSpace d), S a ∂P) ^ g

Jensen's inequality at an affine function of the source scale. The concavity of x ↦ x^g on the nonnegative reals moves the mean of the source inside the power; the printed proof performs this step with Hölder.

The pathwise bound at a cell centered in the unit cube

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_standardCell_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (k : ℤ) {v : Fin d → ℤ} (hv : ∀ (i : Fin d), |standardCellCenter k v i| < 1) : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (coarseBlock (standardCell d k v) a) (blockScale ((3 * 3 ^ (-k) + 1 + 3 * (3 ^ (-k) * S a)) ^ g) E)

The pathwise Euclidean cell bound. The random-source ellipticity of e.coarse.ellipticity read at the macroscopic generation max{1, k+l}, where 3^l brackets 3^{-k}S: a standard aligned cube whose center lies in the unit cube is inside every macroscopic cube of generation at least one, so no factor of the target's generation is produced.

Integrability and the mean bound

theorem HCPolySupport.HighContrast.Entry.hasIntegrableCoarseBlock_standardCell {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (k : ℤ) {v : Fin d → ℤ} (hv : ∀ (i : Fin d), |standardCellCenter k v i| < 1) : HasIntegrableCoarseBlock P (standardCell d k v)

The coarse response over a standard aligned cube is integrable over the law at every generation and every aligned center.

theorem HCPolySupport.HighContrast.Entry.annealedBlock_standardCell_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) (k : ℤ) (w : Fin d → ℤ) : BlockMatLoewnerLE (annealedBlock P (standardCell d k w)) (blockScale ((1 + 9 * K ^ 2 * 3 ^ (-k)) ^ g) E)

The Euclidean cell bound at every generation and every center. The mean of the coarse response over a standard aligned cube of generation k lies below (1 + 9K_{Ψ_S}^23^{-k})𝐄 to the power g, uniformly in the aligned center: the cube is an integer translate of one centered in the unit cube, and there the random-source ellipticity applies with no macroscopic loss.

theorem HCPolySupport.HighContrast.Entry.hasIntegrableCoarseBlock_standardCell_of_stationary {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) (k : ℤ) (w : Fin d → ℤ) : HasIntegrableCoarseBlock P (standardCell d k w)

The coarse response over a standard aligned cube is integrable over the law at every generation and every aligned center: the finiteness at the reduced center transports along the integer translation.