High-contrast homogenization: Entry.Response.Kernel.EllipticRepresentativeInputs #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Elliptic representatives and integrability inputs #
For the recentred coefficients a_- = respCoeffMinus F a and a_+ = respCoeffPlus F a, this file
produces an almost-everywhere-equal representative that is pointwise elliptic on the response
cell, and uses it to obtain MemLp of the pulled-back flux consumed by the cutoff-pairing bound.
It then proves, at the carriers of the diagonal weak-norm estimate, the nonnegativity of the
averaged energy density and the integrability of the doubled optimizer field and its flux, for
both signs and on both the aligned subcells and the parent cell. These are the elliptic and
integrability inputs of the response-transfer estimate p.response.transfer.
The elliptic input for the cutoff bound, and the pulled-back flux it feeds #
IsEllipticFieldOn lam Lam (adaptedCell q t) b is a hypothesis that the cutoff bound
(integral_abs_cutoffPairingOnCell_le_respWeak,
HCPoly/Entry/Response/Cutoff/ResponseTransferFromCutoffBound.lean) does not carry and
would have to be given one, in order to reach
MemLp flux 2 (normalizedCubeMeasure Q) for the pulled-back flux -- the hflux slot of the
generic CG product bridge
abs_cubeAverage_vecDot_centered_scalar_cutoff_le_scaledWeakNormProduct in namespace
Book.Ch05.Section53.JUpperBoundWeakNorms.
It does not have to be given one. For the two coefficients the cutoff bound actually
quantifies over,
respCoeffMinus F a and respCoeffPlus F a with a : CoeffSpace d, the datum is DERIVABLE from
a's own qualitative local uniform ellipticity (HCPoly/Setup/CoefficientSpace.lean) together
with the invertibility of the grid, which the cutoff bound carries through its premise
2 * d ≤ 3 ^ jStar. The derivation is
Annealed.exists_elliptic_representative_adapted
(HCPoly/Entry/Annealed/AdaptedDomainLocality.lean)
followed by isEllipticFieldOn_sub_skew/isEllipticFieldOn_transpose_add_skew; it is exactly the
derivation already performed inside bddAbove_respWeakEnergySet_respCoeffMinus
, lifted here to a reusable statement.
The shape is the a.e.-REPRESENTATIVE one -- ellipticity of some f with
respCoeffMinus F a =ᵐ f on the cell -- and not ellipticity of respCoeffMinus F a on the nose,
because a point of CoeffSpace d is an a.e. class and no representative of it is elliptic
pointwise. This is the same shape as the bddAbove_respWeakEnergySet hypothesis
and as
CoeffSpace.exists_pointwise_coeffOn_family_aeeq, and it is
enough for every MemLp/Integrable consumer, all of which are a.e. invariant.
The elliptic representative on an adapted cell, for both response coefficients #
The elliptic input for the cutoff bound, minus sign. For every sample a the coefficient
a_- = a - g has, on the adapted cell, an a.e.-equal representative that is uniformly elliptic
there. Nothing but invertibility of the grid is needed; the constants belong to the sample and
to the cell and enter no estimate, since the ellipticity is qualitative and local.
The elliptic input for the cutoff bound, plus sign. The transposed twin, for a_+ = a^t + g.
The same datum at the cutoff bound's own grid, from its own premises:
2 * d ≤ 3 ^ jStar and positive definiteness of the canonical metric.
The plus twin of the previous.
The pulled-back flux is L² for the normalized reference-cube measure #
The flux slot of the pulled-back centred optimizer field. The field
y ↦ q⁻¹ ((optimizerField b u (q y) − Y).2) is square integrable for
the normalized measure of the reference cube — the hflux slot of the generic CG product bridge
abs_cubeAverage_vecDot_centered_scalar_cutoff_le_scaledWeakNormProduct
(Book/Ch05/.../JUpperBoundWeakNorms/Product/Bridge.lean), whose potential slot is
respCenteredPullbackH1 (AffineSobolevPullback.lean).
The elliptic datum is taken in the a.e.-representative form produced by
exists_elliptic_representative_respCoeffMinus/…Plus above, so the cutoff bound needs no
ellipticity
hypothesis of its own.
Pointwise ellipticity and integrability of the recentred field at the carriers #
Every cell-average step of the diagonal weak-norm estimate moves a matrix through the cell
average of the doubled optimizer field optimizerField b u = (∇v, b ∇v), so those steps ask
for two things about the recentred coefficient b = respCoeffMinus F a (or b = respCoeffPlus F a): uniform ellipticity of b on the cell and integrability of both slots of the doubled
field.
Pointwise ellipticity is not derivable. A point of CoeffSpace d is an a.e. class, while
IsEllipticFieldOn lam Lam U b requires IsEllipticMatrix lam Lam (b x) at every x ∈ U; an
arbitrary representative of the class may be modified on a null set and remain locally uniformly
elliptic almost everywhere, so only the a.e. shape IsAEEllipticFieldOn lam Lam U b is
available. The tree carries the a.e.-representative datum for the two response coefficients,
exists_elliptic_representative_respCoeffMinus and …Plus (EllipticRepresentativeInputs.lean):
some
field f pointwise elliptic on the cell and equal to b there almost everywhere.
This file discharges the integrability side conditions through that representative. Integrals
are a.e. invariant, so the representative suffices. The flux slot x ↦ b(x) ∇u(x) is L²
because the representative's flux is L² (memVectorL2_matVecMul_of_isEllipticFieldOn) and the
two agree almost everywhere; the scalar energy density ∇u · b ∇u is the vecDot pairing of
two L² fields (integrableOn_vecDot_of_memVectorL2); and it is nonnegative almost everywhere
because the representative is elliptic on the cell, so the vecDot against its lower bound is
a.e. nonnegative and volumeAverage inherits that sign.
Transport of the flux and the energy density across the a.e. representative #
The flux slot is L² through the a.e. representative. If b agrees almost everywhere
on a set U with a field f pointwise elliptic on a subset V ⊆ U, then x ↦ b(x) ∇u(x) is
L² on V for any AHarmonicFunction of b on U: the representative's flux is L² there
and the two coincide a.e. on V.
The scalar energy density is integrable through the a.e. representative. If b agrees
almost everywhere on U with a field f pointwise elliptic on U, then
x ↦ ∇u(x) · b(x) ∇u(x) is integrable on U: the gradient is L² and the representative's
flux is L², so their vecDot pairing is L¹, and the a.e. equality transports it to b.
The averaged energy density is nonnegative through the a.e. representative. If b
agrees almost everywhere on a measurable set U with a field f pointwise elliptic on U
with lower constant lam > 0, then the volume average over U of
x ↦ ∇u(x) · b(x) ∇u(x) is nonnegative. On the full-measure set where b = f, the integrand
is bounded below by lam * ‖∇u(x)‖², hence nonnegative, and integral_nonneg_of_ae gives the
sign of the average.
The recentred coefficient a_- = respCoeffMinus F a #
Integrability of both slots of the doubled optimizer field on a triadic subcell, for
respCoeffMinus F a. For an invertible grid q, generation t and depth n, both slots of
the doubled optimizer field of an arbitrary AHarmonicFunction attached to respCoeffMinus F a
on HighContrast.adaptedCell q t are integrable on every aligned depth-n subcell
adaptedCellAtCenter q (t - n) w. The gradient slot needs no ellipticity; the flux slot uses the
a.e.-elliptic representative on the subcell.
Integrability of the scalar energy density on the parent cell, for
respCoeffMinus F a. The energy density x ↦ ∇u(x) · (respCoeffMinus F a)(x) ∇u(x) of an
arbitrary AHarmonicFunction attached to respCoeffMinus F a on the adapted cell is integrable
there.
Nonnegativity of the averaged energy density, for respCoeffMinus F a. The volume
average over the adapted cell of the energy density of an arbitrary AHarmonicFunction attached
to respCoeffMinus F a is nonnegative.
The transposed recentred coefficient a_+ = respCoeffPlus F a #
Integrability of both slots of the doubled optimizer field on a triadic subcell, for
respCoeffPlus F a. The transposed twin of
integrableOn_optimizerField_respCoeffMinus_box.
Integrability of the scalar energy density on the parent cell, for respCoeffPlus F a.
The transposed twin of integrableOn_energyDensity_respCoeffMinus.
Nonnegativity of the averaged energy density, for respCoeffPlus F a. The transposed
twin of energyDensity_average_nonneg.