High-contrast homogenization: Provider.Entry.EuclideanAdapter

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

The Euclidean inputs of the adapted-to-Euclidean comparison

The proof of the comparison between adapted and Euclidean cubes decomposes each cell of one grid into cells of the other and reads the resulting boundary layers in two regimes: the layers at generations at or above the comparison scale are handled by integer stationarity, the layers below it by the random-source ellipticity together with the source moment. This file proves the Euclidean-side input of each regime, both unconditionally in the generation.

Below the comparison scale. The ellipticity of e.coarse.ellipticity bounds the response of a centered cube of generation i by 3^{g(m-i)}𝐄 at every macroscopic generation m ≥ i that has burned the source. Taking m to be the smallest such triadic generation gives the pathwise bound 𝐀(□_i) ≤ (1 + 3·3^{-i}S)^g𝐄, and Jensen's inequality for the concave x ↦ x^g — the step the printed proof performs with Hölder — turns its mean into (1 + 6K_{Ψ_S}^23^{-i})^g𝐄. The cube being centered at the origin, the macroscopic containment costs nothing, so no factor of the generation survives.

At or above the comparison scale. Centered cubes are the adapted cells of the identity grid, which the rounded adapted grid of s.scale.selection fixes at every nonnegative alignment, so the annealed mean order of p.fixed.geometry.parent.child.recurrence reads on them directly: F_p ≤ F_j whenever k_0(d) ≤ j ≤ p. Finiteness at every generation is itself a consequence of e.coarse.ellipticity, so no window enters.

There are no definitions in this file.

The Euclidean generation bound

theorem HCPolySupport.HighContrast.Entry.exists_pow_three_bracket {x : ℝ} (hx : 0 ≤ x) : ∃ (l : ℕ), x ≤ 3 ^ ↑l ∧ 3 ^ ↑l ≤ 1 + 3 * x

A natural power of three that dominates a nonnegative real and is itself dominated by 1 + 3x.

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_centeredCube_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (i : ℤ) : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (coarseBlock (centeredCube d i) a) (blockScale ((1 + 3 * (3 ^ (-i) * S a)) ^ g) E)

The pathwise Euclidean generation bound. The random-source ellipticity of e.coarse.ellipticity, read at the smallest triadic macroscopic scale above both the generation and the source scale; the argument being centered at the origin, the macroscopic containment costs nothing.

theorem HCPolySupport.HighContrast.Entry.integral_rpow_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) {c : ℝ} (hc : 0 ≤ c) : ∫ (a : CoeffSpace d), (1 + c * S a) ^ g ∂P ≤ (1 + c * ∫ (a : CoeffSpace d), S a ∂P) ^ g

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

theorem HCPolySupport.HighContrast.Entry.annealedBlock_centeredCube_le_blockScale {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (i : ℤ) : BlockMatLoewnerLE (annealedBlock P (centeredCube d i)) (blockScale ((1 + 6 * K ^ 2 * 3 ^ (-i)) ^ g) E)

The Euclidean generation bound. The annealed block of the centered cube of generation i is below (1 + 6K_{Ψ_S}^23^{-i})^g times the reference block, at every generation.

The Euclidean mean order

theorem HCPolySupport.HighContrast.Entry.roundedGrid_one_of_nonneg {d : ℕ} [Nonempty (Fin d)] {j : ℤ} (hj : 0 ≤ j) : roundedGrid j 1 = 1

The identity witness is fixed by the rounding of s.scale.selection at every nonnegative alignment.

theorem HCPolySupport.HighContrast.Entry.isRoundedGrid_one {d : ℕ} [Nonempty (Fin d)] : IsRoundedGrid (↑(kZero d)) 1

The identity grid is a rounded adapted grid at the rounding scale.