High-contrast homogenization: Analytic.WeakGradientClosure #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The weak-gradient relation is an identity between convergent integrals #
HasWeakGradientOn U u Du compares two Bochner integrals. A Bochner integral
of a non-integrable integrand is 0, so a pair whose pairings all diverge
satisfies the relation as 0 = -0, saying nothing. The disposition taken here
is not to change the relation but to prove that this branch is unreachable on
the classes the homogenization theorem actually reads: for a member of
H¹_{s,loc}(ℝ^d) and a local test on a centred ball, both pairings converge
absolutely, so the relation is an identity between genuine integrals.
The hypotheses used are exactly the coefficient class hypotheses 0 < lam and
almost-everywhere ellipticity, the measurability of the pair, and membership in
the local class. The ellipticity assumption is not removable: on a field
that vanishes identically every weighted energy vanishes, and the class then
constrains the gradient field by nothing beyond measurability. At the places
t.random.homogenization reads these classes the field is
a member of the coefficient space, whose defining condition supplies exactly
those two hypotheses; the class-level wrappers at the end of the module state
the results in that form.
The final group of lemmas records what the measurability condition of the class buys. A function invisible to both the lower Lebesgue integral and the Bochner integrals lands in the class with zero weak gradient whatever its measurability; with the measurability condition present the same construction is degenerate, producing only the zero function. Whether the wider class without that condition is strictly wider is a question about sets of inner measure zero and is not settled here: the possibility that the two classes coincide is not ruled out, so the construction below may be vacuous.
Absolute convergence of both pairings #
The closure lemma. For a pair of the local class and a local test on a
centred ball, both pairings of the weak-gradient relation are absolutely
convergent. The branch valuing a non-integrable integrand at 0 is therefore
unreachable on this class.
Hypotheses used, in full: local uniform ellipticity of the coefficient field,
whose constants are read on the ball; almost everywhere strong measurability of
v and of the components of Dv on the ball; membership in MemH1sLoc; and φ
a local test on the ball.
The closure, in the form the weak-gradient relation is read. Both
pairings converge absolutely and the identity holds between them. This is
the statement that the 0 = -0 branch is not what membership in the local class
is asserting.
The localized form at V = Set.univ. A local test on all of ℝ^d has
compact support, so the ball form transfers.
What the measurability condition of the class buys #
The class sees v only through
- the lower Lebesgue integral
∫⁻ x in V, ENNReal.ofReal |w n x - v x|, which is a supremum over simple functions below the integrand and is therefore blind to any perturbation supported on a set of inner measure zero; and - the Bochner integrals of
HasWeakGradientOn, which value a non-integrable integrand at0.
The two lemmas below make the reduction formal: any v that is invisible to
both lands in the local class with zero weak gradient, whatever its
measurability. Instantiating with the indicator of a Bernstein set B ⊆ ℝ^d
— every measurable subset of B and of Bᶜ is null, so B has inner measure
0 and full outer measure in every open set — would give a member of the wider
class that is not almost everywhere strongly measurable, hence not integrable on
any ball. Bernstein sets are a ZFC construction and are not in Mathlib, so that
half is cited rather than formalized, and the possibility that the two classes
coincide is not ruled out here.
The coordinate gradient of a constant vanishes.
A function whose lower Lebesgue integral vanishes on every ball, and whose weak gradient is zero there, lies in the local class with zero gradient field, for every coefficient field.
With the measurability condition present as a hypothesis the conclusion is degenerate: those hypotheses together force the function to vanish almost everywhere, so this construction exhibits nothing but the zero function. It is kept because it is the shape available before the class carried that condition, and the difference between the two readings is exactly what the condition buys.
A function that is not almost everywhere measurable on a set is not integrable there. This is the contraposed measurability half of integrability, and it is recorded only because it is the step at which a pair failing the class's measurability condition is separated from the integrable ones; it says nothing on its own about either the class or the reference text's spaces.
The class-level statements #
The local class carries the measurability of its pair, so the statements above may be restated with their measurability hypotheses discharged from the class itself. What remains assumed is the coefficient field, through local uniform ellipticity: on every bounded set a pair of constants for that set.
A member of the local class is integrable on every centred ball.
Both pairings of the weak gradient relation converge absolutely for a member of the local class, on every centred ball.
The same on the whole space, which is where the corrector equation of
t.random.homogenization is read.