High-contrast homogenization: Analytic.ClosureH1a #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The closure family of H¹_a(V) and H¹_{a,0}(V) #
The relation tying a function to its weak gradient is an identity between two
pairings against a test function. Read without a convergence guard it is
satisfied vacuously — as 0 = -0 — by a pair both of whose pairings diverge.
The statements collected here are what makes that branch unreachable on the
coefficient-Sobolev classes of s.introduction: the function
slot of a member is of finite L¹ mass and integrable, and the gradient slot is
square integrable with integrable components.
The two classes differ in exactly one place. The approximants of H¹_a(V) are
globally smooth and nothing bounds them on an unbounded V, so that half
carries Bornology.IsBounded V; the approximants of H¹_{a,0}(V) are compactly
supported inside V, so that half carries no hypothesis on V at all. The
step from square integrability of the gradient to integrability of one of its
components needs only that V have finite measure, which is strictly weaker
than boundedness.
The module closes with the gradient side of the local class H¹_{s,loc}(ℝ^d),
which is square integrable on every centred ball and has integrable components
there and on every compact set.
Shared scaffolding #
Two facts the closure statements below need and the two-sided energy comparison
does not supply: the scalar counterpart of
lintegral_ofReal_vecNormSq_ne_top_of_hasCompactSupport, and the extension of
an integrability statement from a measurable subset to a superset across which
the integrand vanishes. The latter is stated without measurability of the
superset — it is the restriction identity (μ|_V)|_K = μ|_{K ∩ V} = μ|_K, not a
difference-set argument.
A continuous function with compact support has finite L¹ mass on every
set, with no hypothesis on the set.
Integrability transfers from a measurable subset to any superset across which the integrand vanishes. No measurability of the superset is used.
The function slot against a test gradient: an L¹ function times the bounded
gradient of a local test.
The gradient slot against a test: a field that is L² on V pairs
absolutely with a local test. The pairing is read on the compact support of the
test, which has finite measure whatever V is, so neither boundedness nor
measurability of V enters.
The H¹_a(V) and H¹_{a,0}(V) closure family #
The mirror, for the two global classes, of what the local class H¹_{s,loc}
already has. The two classes differ in exactly one place: the approximants of
MemH1a are globally smooth and nothing bounds them on an unbounded V, so the
H¹_a half carries Bornology.IsBounded V, while the H¹_{a,0} half — whose
approximants are compactly supported inside V — carries no hypothesis on V
at all.
The measurability of the function slot, read off the class.
The measurability of the gradient slot, read off the class.
The measurability of the function slot of H¹_{a,0}, read off the class.
The measurability of the gradient slot of H¹_{a,0}, read off the class.
The L¹ half of the H¹_a(V) class is honest on a bounded V, with no
measurability input at all: the lower Lebesgue integral of |u| over V is
finite.
Boundedness of V is not removable: MemH1a is an approximability condition
and a globally smooth u approximates itself at distance 0 whatever its
growth (exists_memH1a_sEnergyOn_eq_top runs the same argument for the energy
slot).
The L¹ half of the H¹_{a,0}(V) class is honest on an arbitrary V:
the approximants are compactly supported inside V, so no hypothesis on V is
needed.
A member of H¹_a(V) is integrable on a bounded V. The measurability
conjunct is read off the class; the finiteness is the previous lemma.
The gradient slot of H¹_a(V) is square integrable on a bounded V.
The gradient slot of H¹_{a,0}(V) is square integrable on an arbitrary
V.
The components of the gradient slot of H¹_a(V) are integrable on a
bounded V. The step from L² to L¹ is the finiteness of the measure of
V, which boundedness already supplies.
The components of the gradient slot of H¹_{a,0}(V) are integrable on a
V of finite measure. Finiteness of the measure is the only thing the step
from L² to L¹ needs, and it is strictly weaker than boundedness.
The gradient slot of the local class #
The function slot v of MemH1sLoc is closed on every centred ball by the
local family; the gradient slot Dv is not. The step from the class's finite
weighted energy to L¹ of a component is the finiteness of the measure of the
ball, and the ellipticity pair converting the weighted energy into the
unweighted one is read on that ball as well.
The gradient slot of H¹_{s,loc} is square integrable on every centred
ball.
The components of the gradient slot of a member of the local class are integrable on every centred ball.
The same on every compact set, which is the form the whole-space reading needs.