High-contrast homogenization: MainResults #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Main results #
The headline theorems of the formalization of the paper HCPolySupport at a polynomial scale in high contrast (Armstrong--Kuusi--Loher), stated here in full. Each is proved by direct application of the theorem it restates, so the statement displayed in this file is the one that has been checked.
HCPoly.polynomial_entry-- Theorem A of the paper,t.polynomial.entry: entry into the small-contrast regime at every generation beyond a multiple of the base-three logarithm of2 + Π K, hence at a length polynomial in the reference aspect ratio and in the growth constant of the source tail.HCPoly.algebraic_convergence-- Theorem B of the paper,t.algebraic.convergence: beyond a generation bounded by a multiple of the base-three logarithm of2 + Π K, the annealed contrast decays geometrically and the annealed blocks converge, in the Loewner order and at the same rate, to a deterministic self-dual positive definite limit block.HCPoly.uniform_homogenization-- Theorem C of the paper,t.uniform.homogenization: the uniformly elliptic model, obtained as the instance of Theorem D at exponent zero with a vanishing source scale, with a homogenization scale whose tail isexp(-t^d)beyond a length polynomial in the ellipticity ratio.HCPoly.polynomial_homogenization-- Theorem D of the paper,t.random.homogenization: quantitative homogenization, first-order correctors, a Liouville theorem and large-scale regularity above a single random radius whose tail has a stretched-exponential term and a rescaled copy of the source tail.HCPoly.quenched_convergence-- quenched convergence of the coarse-grained matrices: the estimate used in the proof of Theorem D in the subsectionss.random.dirichlet. It is not one of the theorems of the introduction.
All five reduce to the standard axioms
(propext, Classical.choice, Quot.sound).
Theorem A: polynomial entry into small contrast #
Theorem A, t.polynomial.entry: polynomial entry into small contrast.
Fix a dimension d ≥ 2, a coarse ellipticity exponent g ∈ [0, 1) and a
tolerance σ ∈ (0, 1]. There is a constant C, depending on these three data
alone -- in particular independent of the reference block, of the coefficient
law, of the reference aspect ratio e.reference.aspect.ratio and of the growth
constant of the source tail -- such that for every stationary law of unit range
of dependence which is coarsely elliptic above its random source scale the
annealed contrast e.Theta.m is at most 1 + σ at every generation beyond the
entry generation ⌈C log₃(2 + Π K)⌉ of e.polynomial.entry. The length of that
entry generation is polynomial in the reference aspect ratio and in the growth
constant of the source tail.
No bound uniform as g increases to one is asserted.
Theorem B: algebraic convergence at a polynomial scale #
Theorem B, t.algebraic.convergence: algebraic convergence at a
polynomial scale. Fix a dimension d ≥ 2 and a coarse ellipticity exponent
g ∈ [0, 1). There are constants C and κ, depending on these two data
alone, such that every stationary law of unit range of dependence which is
coarsely elliptic above its random source scale admits a deterministic
generation m₀ subject to the bound e.algebraic.entry, beyond which the
annealed contrast e.Theta.m decays geometrically at rate κ
(e.algebraic.contrast.decay), and a deterministic symmetric positive definite
limit block Abar which the annealed blocks of the centred cubes approach from
above in the Loewner order at the same rate, with the constant six of
e.algebraic.block.decay.
The Schur coefficients of the limit block, in the parametrization
e.annealed.schur, satisfy s_bar_* = s_bar, with s_bar positive definite and k_bar
antisymmetric; ā = s_bar + k_bar is the coefficient matrix associated with the law.
The coefficient fields are locally uniformly elliptic almost everywhere, with
ellipticity constants belonging to the field and entering no estimate; the
paper's standing condition e.qualitative.ellipticity expresses this through
local essential bounds on the symmetric and skew parts, and every quantitative
object below is independent of the local ellipticity constants.
Theorem C: quantitative homogenization under uniform ellipticity #
Theorem C, t.uniform.homogenization: quantitative homogenization under
uniform ellipticity. For a ℤ^d-stationary law of unit range whose fields
satisfy e.uniform.ellipticity with 0 < λ ≤ 1 ≤ Λ there are a homogenized
matrix with positive definite symmetric part, a corrector family, and a
homogenization scale X ≥ 1 whose tail is e.uniform.scale.tail: the exponent
is the dimension, and the deterministic factor in front of t is a power of
2 + Λ/λ with a dimensional exponent. On one translation invariant event of
full probability the Dirichlet estimate and the large-scale energy estimate
e.uniform.energy hold. The Lean theorem also exports the corrector equation
and estimate, the Liouville classification and the first-order approximation
from its specialization of Theorem D; these are not clauses of the paper's
printed Theorem C.
This is the instance of Theorem D, t.random.homogenization, for uniformly
elliptic laws: the coarse ellipticity condition holds at the exponent g = 0
with a vanishing source scale and the reference block diag(2Λ, 2λ⁻¹), whose
reference aspect ratio is at most 4Λ/λ, so the two-part tail collapses to
exp(-t^d) and the length (2 + Π K)^C becomes (2 + Λ/λ)^C.
Differences from the printed statement. The Dirichlet clause is the
homogeneous negative-Sobolev estimate of Theorem D on the adapted cells of the
homogenized matrix, not the L² estimate e.uniform.dirichlet with a forcing
term on the ellipsoids e.homogenized.ellipsoids; the paper deduces the latter
from the former by a separate duality argument, which is not formalized. The
tolerance δ of that estimate is accordingly absent, and the endpoint constant
is the shape constant of Theorem D. The large-scale energy estimate and the
first-order approximation are stated on the ellipsoids of
e.homogenized.ellipsoids, with the constant C of the tail; the other
differences listed for Theorem D apply unchanged.
Theorem D: homogenization with a random source scale #
Theorem D, t.random.homogenization: homogenization with a random source
scale. Under the standing assumptions there are a homogenized matrix with
positive definite symmetric part, a length bounded by a power of 2 + Π K, and
a measurable random radius whose tail is the two-part bound
e.random.scale.tail, together with a slope-linear family of stationary
corrector gradients, such that almost surely and simultaneously: the Dirichlet
estimate e.random.dirichlet holds for every microscale below the radius; the
correctors solve the corrector equation and obey e.random.corrector; the
entire solutions of the growth condition e.random.liouville.growth are exactly
the affine functions corrected by the family; and the large-scale energy and
excess-decay estimates e.random.energy and e.random.regularity hold above
the radius.
The coefficient class. The coefficient fields are locally uniformly
elliptic almost everywhere, with ellipticity constants belonging to the field
and entering no estimate below; the paper's standing condition
e.qualitative.ellipticity expresses this through local essential bounds on
the symmetric and skew parts. Every quantitative object below -- the
reference aspect ratio, the gauge and its growth witness, the homogenized
matrix, the length and its tail, and every dimensional constant and exponent --
is independent of those constants.
Differences from the printed statement.
- The random radius satisfies
1 ≤ X, where the paper statesX ≥ max {1, S}. - The homogenized matrix is produced existentially, rather than identified with
the matrix of Theorem B,
t.algebraic.convergence. - The domains carrying the Dirichlet estimate are the adapted cells of the homogenized matrix -- translates of the image of a centred triadic cube under the symmetric square root of its symmetric part -- normalized to sit between two concentric adapted ellipsoids, rather than the bounded Lipschitz domains of the paper. Every domain the development uses is such a cell; the normalization fixes the size of the domain relative to the homogenized matrix, which is the scale the endpoint constant would otherwise have to carry, and it is satisfiable at every dimension because the window between the two ellipsoids has triadic ratio three.
- The two flux differences -- in the Dirichlet estimate and in the corrector estimate -- are written for the skew-centered field: the constant skew part of the homogenized matrix is subtracted from the coefficient field, and the homogenized matrix enters through its symmetric part. This is the standing convention under which a coefficient field and its antisymmetric part are read modulo a constant antisymmetric matrix; it is the form the argument establishes, a constant skew part changing neither the solutions nor the coarse-grained blocks, and it is the form invariant under that recentering, which the displays written with the full homogenized matrix are not.
- All norms and energies are valued in
ℝ≥0∞, so that each estimate is an assertion about the quantity the paper writes rather than about a totalized integral that vanishes when that quantity is infinite. - The endpoint constant of the Dirichlet estimate depends on nothing but the dimension, the regularity exponent and the shape of the adapted domain -- the radii of concentric balls trapping it -- so its binder stands outside the exponent and outside the law. The two radii enter only through their ratio: dilating the coefficient field and the homogenized matrix together leaves the condition on the domain fixed, slides both radii along a common ray, and multiplies both sides of the estimate by the same factor.
- The constants
C,C₀andC₁are asserted positive, where the paper asserts only their finiteness; positivity is a normalization, every occurrence of each being weakened by increasing it. - The three membership classes carry the measurability of the function and of its gradient field that their printed counterparts -- completions of smooth functions in a norm -- presuppose. The second inclusion of the Liouville clause is the only place this statement says anything about the measurability of the corrector family, and it is what puts the correctors in the local class.
- The coefficient-weighted spaces are closures under globally smooth approximants, where the paper closes the functions smooth on the domain. On a bounded convex domain a function smooth on the domain agrees, after a dilation towards an interior point, with a globally smooth function on the whole closure, so the two readings are separated only by the continuity of that dilation in the norm.
- The invariance of the full-probability event under integer translations is carried in the conclusion; the paper does not state it.
Quenched convergence of the coarse-grained matrices #
Quenched convergence of the coarse-grained matrices. The estimate the
proof of Theorem D uses in the subsection ss.random.dirichlet; it is not one
of the theorems of the introduction.
There are a deterministic symmetric positive definite limit block pinning the
annealed blocks of the centred cubes from both sides, a length bounded by a
power of 2 + Π K, and a measurable random scale whose tail is the two-part
bound e.random.scale.tail, such that on one translation-invariant event of
full probability the weighted sum over depths of the largest normalized excess
of a coarse-grained block over the limit block, taken over the cells of that
depth inside the outer cube and restricted to the event that the source has
burned at the outer scale, decays algebraically in the ratio of the outer scale
to the random scale, below any prescribed tolerance.
The coefficient fields are locally uniformly elliptic almost everywhere, with
ellipticity constants belonging to the field and entering no estimate; the
paper's standing condition e.qualitative.ellipticity expresses this through
local essential bounds on the symmetric and skew parts, and every
quantitative object below -- the reference aspect ratio, the gauge and its
growth witness, the limit block, the length, the tail, and every dimensional
constant -- is independent of those constants.