High-contrast homogenization: Entry.Response.Core.SubcellCoefficientGluing #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Gluing the recentred coefficient across slices and subcells #
This file glues the per-slice optimizer readouts into the recentred coefficients a_-/a_+ on
the parent adapted cell, and performs the same construction on each aligned adapted subcell,
keeping the raw field definitionally equal to respCoeffMinus/respCoeffPlus. It proves the
resulting measurability of the coefficient carriers, and the cell-energy layer: the metric square
of the canonical state's average on a cell is controlled by the cell's response size and the
actual state energy there. A short addendum records the integrability, on its own subcell, of the
recentred child field the diagonal weak-norm estimate's cell-average step consumes. This is the
gluing and cell-energy layer of the response transfer p.response.transfer.
Gluing optimizer readouts across quantitative slices #
Quantitative slices cover each transformed regular response field on an adapted cell.
Choose a Chapter-2 coefficient object from the first quantitative slice containing a regular field. Its raw representative remains exactly the input field.
Equations
Instances For
Glue the fixed-slice weighted-readout theorem across a measurable countable slice cover.
The actual transformed coefficient fields #
The minus transformed coefficient lies in some quantitative slice on every adapted cell.
The plus transformed coefficient lies in some quantitative slice on every adapted cell.
Canonical Chapter-2 coefficient object for the minus transformed response field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Canonical Chapter-2 coefficient object for the plus transformed response field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Adapted cells have positive real volume, in the exact form used by the Galerkin selector.
Every weighted coordinate readout of the canonical minus optimizer is measurable in the coefficient sample.
Every weighted coordinate readout of the canonical plus optimizer is measurable in the coefficient sample.
Restricting the readout weight by an indicator realizes a localized volume average.
Localized weighted averages of the canonical minus optimizer are measurable.
Localized weighted averages of the canonical plus optimizer are measurable.
The Chapter-2 coefficient object on an aligned adapted subcell #
SubcellCoefficientGluing.lean attaches to the parent adapted cell ⋄_t^q a Chapter-2 coefficient
object whose raw field is the recentred response coefficient a_- = a - g (resp.
a_+ = aᵀ + g), and keeps that raw field definitionally equal to respCoeffMinus (resp.
respCoeffPlus). This module performs the same construction on each aligned adapted subcell
adaptedCellAtCenter q k w, the per-w child carrier of the aligned subdivision.
The elliptic input on the subcell is obtained from
Annealed.exists_elliptic_representative_adapted, which covers every translated adapted cell
adaptedCellTranslate q k y, hence in particular adaptedCellAtCenter q k w. The quantitative
slice
cover then follows from exists_responseSlice_of_ellipticRepresentative.
The elliptic representative on an aligned subcell #
The minus transformed coefficient a_- = a - g has, on the aligned adapted subcell
adaptedCellAtCenter q k w, an a.e.-equal representative that is uniformly elliptic there. The
constants depend on the sample and on the cell only and enter no estimate.
The plus transformed coefficient a_+ = aᵀ + g has, on the aligned adapted subcell
adaptedCellAtCenter q k w, an a.e.-equal representative that is uniformly elliptic there.
The quantitative slice covers on the subcell #
The minus transformed coefficient lies in some quantitative slice on every aligned adapted subcell.
The plus transformed coefficient lies in some quantitative slice on every aligned adapted subcell.
The canonical subcell coefficient objects #
Canonical Chapter-2 coefficient object for the minus transformed response field on the aligned
adapted subcell adaptedCellAtCenter q k w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Canonical Chapter-2 coefficient object for the plus transformed response field on the aligned
adapted subcell adaptedCellAtCenter q k w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Integrability of the recentred child field on its own subcell #
The cell-average head of the diagonal weak-norm estimate consumes an AHarmonicFunction that
already lives on an aligned adapted child adaptedCellAtCenter q k w, not on the parent
HighContrast.adaptedCell q t. This module records, for the recentred coefficients
respCoeffMinus F a and respCoeffPlus F a, the three input facts on that child: integrability
of both slots of the doubled optimizer field, integrability of the scalar energy density, and
nonnegativity of its volume average.
The proofs are the parent-cell arguments re-instantiated at the child. The elliptic
representative is the one already attached to the child
(exists_elliptic_representative_respCoeffMinusAt,
exists_elliptic_representative_respCoeffPlusAt),
so the restriction of an ellipticity statement from the parent is not needed; the generic
transport engines over an a.e. representative do all the work.
The recentred coefficient a_- = respCoeffMinus F a on its child #
Integrability of both slots of the doubled optimizer field on the child, for
respCoeffMinus F a. For an invertible grid q and an aligned adapted child
adaptedCellAtCenter q k w, both slots of the doubled optimizer field of an arbitrary
AHarmonicFunction attached to respCoeffMinus F a on that child are integrable there. The
gradient slot needs no ellipticity; the flux slot uses the a.e.-elliptic representative on the
child.
The transposed recentred coefficient a_+ = respCoeffPlus F a on its child #
Integrability of both slots of the doubled optimizer field on the child, for
respCoeffPlus F a. The transposed twin of
integrableOn_optimizerField_respCoeffMinus_at.
The cell energy layer #
The metric square of the canonical state's average on one cell is controlled by the cell's response size and the actual state energy there. That is the statement proved below for an arbitrary Chapter-2 cell; the aligned-subcell instance is its specialization.
How the statement is expressed #
The conclusion is stated with the blockSqrt (respM0 F) congruence
blockVecDot (R v) (R v) for the metric square, and with the two Loewner inputs k and e
for the two sizes blockSize (adaptedResponse q k w a) E and diagonalWeakMetricFactor m E ^ 2.
So the only genuinely new content at this layer is the STATE side:
- the doubled optimizer state
X = (∇u, a∇u)ofResponseBlockObjects.leanis a Chapter-2 doubled RESPONSE field; - its Chapter-2 energy density is exactly TWICE the optimizer energy density used here; the
factor
2is the doubled formX · 𝐀 X = 2 ∇u · a ∇u, and the same2relatesaverage … (blockVecDot state (𝐀 state))todiagonalWeakEnergy ^ 2 = variationEnergyValue(DiagonalWeakNormState.lean); Book.Ch02.averageVecandcellAverage(ResponseBlockObjects.lean) are the same function (rfl).
The definitions adaptedDomainAt, alignedIndex, coe_alignedIndex and
exists_restrict_solution_adaptedCellAtCenter are NOT needed to state or prove the cell energy
bound, because it is stated over an ARBITRARY Book.Ch02.Domain d. They reappear only in
the aligned-subcell instance, where the subcell domain and the restriction do the work, and
where the geometric alignment fact adaptedCellAtCenter q k w ⊆ adaptedCell q t is taken as a
HYPOTHESIS rather than re-derived.
No new definition #
This module introduces NO definition. The one definition it needs, adaptedDomainAt — the
per-w Chapter-2 domain of an aligned adapted subcell, the twin of adaptedDomain
— is supplied by the imported
ResponseFieldSize.lean, together with its explicit ∃
satisfiability witness, which therefore sits ABOVE every consumer here in import order.
That definition selects no constant: its two fields are the
INEQUALITY-free structural obligations IsOpenBoundedConvexDomain and Nonempty, both of which
are already proved for every adaptedCellAtCenter.
The doubled energy density of an optimizer state #
Book.Ch02.blockMatrixField is the pointwise blockMatrixOfCoeff of the
representative — the two definitions (Book/Ch02/Block.lean and
CoarseGraining/BlockFormalism/Structures.lean) have identical bodies.
The doubled energy density of a primal state. On the doubled state (ξ, Aξ) the
Chapter-2 block form collapses to TWICE the scalar energy density:
(ξ, Aξ) · 𝐀 (ξ, Aξ) = 2 ξ · Aξ.
blockMatVecMul_blockMatrixOfCoeff_primal_of_isUnit_det_symmPart
(CoarseGraining/BlockFormalism/MatrixIdentities.lean) gives 𝐀 (ξ, Aξ) = (Aξ, ξ) on the
nose; the rest is blockVecDot's definition.
The state side — restriction, and membership in the doubled response space #
The doubled optimizer state lies in the cell's response space. Taking the adjoint
solution to be zero in 𝒮(U;a) = {(∇u + ∇u*, a∇u - aᵗ∇u*)} gives X = (∇u, a∇u) ∈ 𝒮(U;a).
The carrier bridges — energy, and the cell average #
The Chapter-2 energy of an optimizer state is TWICE the scalar one. The doubled field
Y = (∇u, a∇u) has ⨍_U (Y · 𝐀 Y) = 2 ⨍_U ∇u · a∇u, and the right-hand average is exactly the
integrand of weakOptimizerEnergy (DiagonalDefectCarriers.lean).
The pointwise step is the doubled energy identity above; it holds at every x ∈ U because
hEll makes a(x) elliptic there, and it is lifted to the average by
Book.Ch02.average_eq_of_ae_eq (Book/Ch02/Dilation.lean) along ae_restrict_mem.
weakOptimizerEnergy squared is the average it is the square root of, as soon as
that average is nonnegative.
The cell average IS the Chapter-2 pair of vector averages. cellAverage
(ResponseBlockObjects.lean) and Book.Ch02.averageVec (Book/Ch02/Response.lean) have identical
bodies once Book.Ch02.average is unfolded to volumeAverage, so this is rfl after the two
field rewrites.
The cell-energy bound on an arbitrary Chapter-2 cell #
The cell energy bound. "The metric square of the canonical state's average on one cell is controlled by the cell's response size and the actual state energy there."
It is stated over an ARBITRARY Chapter-2 cell U, so that both the parent cell
adaptedDomain q hq t and every aligned subcell are
instances.
The three encodings it replaces:
metricBlockNormSq m (…)becomes theblockSqrt (respM0 F)congruenceblockVecDot (R v) (R v)(RecentScaleEnergyRoute.lean);diagonalWeakMetricFactor m E ^ 2becomes the Loewner inputk(SharpOrderEnergyMap.lean);blockSize (adaptedResponse q k w a) Ebecomes the Loewner inpute.
The 2 is the doubled quadratic form: the average identity above shows
⨍_U (X · 𝐀 X) = 2 ⨍_U ∇u · a∇u, and weakOptimizerEnergy ^ 2 is the second average. The
same 2 relates average … (blockVecDot state (𝐀 state)) to
diagonalWeakEnergy ^ 2 = variationEnergyValue (DiagonalWeakNormState.lean).
The aligned-subcell instance #
The cell energy bound above is stated over an arbitrary Chapter-2 cell, so the only thing an
aligned subcell needs is its Chapter-2 domain, adaptedDomainAt. That definition is NOT
introduced here. It and its satisfiability witness live in
ResponseFieldSize.lean, which this module imports, so
the witness sits strictly ABOVE every consumer in import order.
The copy of adaptedDomainAt that stood here has been deleted as a duplicate. The two copies
were signature-identical and differed only in how the Nonempty field was proved, which is a
Prop. This module now introduces NO definition of its own.
The cell energy bound on an aligned adapted subcell, for the PARENT optimizer. The
left-hand side is the cell average of the PARENT state
X_t = (∇u, a∇u) over the subcell, and the right-hand side is the actual state energy THERE,
carried by the restricted solution z (hz : z.grad = u.grad).
The obtain ⟨z, hz⟩ := exists_restrict_solution_adaptedCellAtCenter … step is exactly hz here.
The geometric alignment fact adaptedCellAtCenter q k w ⊆ adaptedCell q t is NOT re-derived here:
it is taken as a hypothesis, and this statement does not need it at all, because hz already
carries its consequence.